| ⊢ | w ∧ f ⊃ f1 ⇒ ⊢ w ∧ (f1 g) ⊃ (f g) | StateAndYieldsImpYields |
Proof:
1 | ⊢ w ∧ f ⊃ f1 | given |
2 | ⊢ w ∧ (f ; ¬g) ⊃ f1 ; ¬g | |
3 | ⊢ w ∧¬(f1 ; ¬g) ⊃¬(f ; ¬g) | |
4 | ⊢ w ∧ (f1 g) ⊃ (f g) | 3, def. of |
qed