| ⊢ (f ∨ f1) ⌢ g ≡ (f ⌢ g) ∨ (f1 ⌢ g) | OrChopEqv |
The proof for ⊃ is immediate from axiom OrChopImp.
Here is the proof for ⊂:
1 | f ⊃ f ∨ f1 | |
2 | f ⌢ g ⊃ (f ∨ f1) ⌢ g | |
3 | f1 ⊃ f ∨ f1 | |
4 | f1 ⌢ g ⊃ (f ∨ f1) ⌢ g | |
5 | (f ⌢ g) ∨ (f ⌢ g1) ⊃ (f ∨ f1) ⌢ g |
qed