| ⊢ | (f ∧ f1) ; g ⊃ f ; g | AndChopA |
Proof:
1 | ⊢ f ∧ f1 ⊃ f | |
2 | ⊢ (f ∧ f1 ⊃ f) | |
3 | ⊢ (f ∧ f1 ⊃ f) ⊃ (f ∧ f1) ; g ⊃ f ; g | |
4 | ⊢ (f ∧ f1) ; g ⊃ f ; g |
qed
The following related theorem has a similar proof: