| ⊢ (g ⊃ g1) ⊃ (f ⌢ g) ⊃ (f ⌢ g1) | BoxChopImpChop |
Proof:
1 | finite ⊃ (f ⊃ f) | |
2 | (f ⊃ f) | |
3 | (f ⊃ f) ∧ (g ⊃ g1) ⊃ (f ⌢ g) ⊃ (f ⌢ g1) | |
4 | (g ⊃ g1) ⊃ (f ⌢ g) ⊃ (f ⌢ g1) |
qed