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