| ⊢ | g ⊃ g1 ⇒ ⊢ f ; g ⊃ f ; g1 | RightChopImpChop |
Proof:
1 | ⊢ g ⊃ g1 | given |
2 | ⊢ (g ⊃ g1) | |
3 | ⊢ (g ⊃ g1) ⊃ (f ; g) ⊃ (f ; g1) | |
4 | ⊢ f ; g ⊃ f ; g1 |
qed
Here is a derived rule that is a corollary of RightChopImpChop: