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