| ⊢ | f ∧ (g ; g1) ⊃ (f ∧ g) ; (f ∧ g1) | BaAndChopImport |
Proof:
1 | ⊢ f ⊃ f | |
2 | ⊢ f ∧ (g ; g1) ⊃ (f ∧ g) ; g1 | |
3 | ⊢ f ⊃ f | |
4 | ⊢ f ∧ (f ∧ g) ; g1 ⊃ (f ∧ g) ; (f ∧ g1) | |
5 | ⊢ f ∧ (g ; g1) ⊃ (f ∧ g) ; (f ∧ g1) |
qed