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