| ⊢ f ⊃ f1 ⇒ ⊢ (f ⌢ g) ⊃ (f1 ⌢ g) | LeftChopImpChop |
Proof:
1 | f ⊃ f1 | Assump |
2 | (f ⊃ f1) | |
3 | (f ⊃ f1) ⊃ (f ⌢ g) ⊃ (f1 ⌢ g) | |
4 | f ⌢ g ⊃ f1 ⌢ g |
qed