| ⊢ | f ; (g ∨ g1) ≡ f ; g ∨ f ; g1 | ChopOrEqv |
The proof for ⊂ is immediate from axiom ChopOrImp.
Here is the proof for the converse:
1 | ⊢ g ⊃ g ∨ g1 | |
2 | ⊢ f ; g ⊃ f ; (g ∨ g1) | |
3 | ⊢ g1 ⊃ g ∨ g1 | |
4 | ⊢ f ; g1 ⊃ f ; (g ∨ g1) | |
5 | ⊢ f ; g ∨ f ; g1 ⊃ f ; (g ∨ g1) |
qed