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