| ⊢ | g ⊃ g1 ⇒ ⊢ (f g) ⊃ (f g1) | RightYieldsImpYields |
Proof:
1 | ⊢ g ⊃ g1 | given |
2 | ⊢ ¬g1 ⊃¬g | |
3 | ⊢ f ; ¬g1 ⊃ f ; ¬g | |
4 | ⊢ ¬(f ; ¬g) ⊃¬(f ; ¬g1) | |
5 | ⊢ (f g) ⊃ (f g1) | 3, def. of |
qed