| ⊢ f ∧ (f1 ⌢ g) ⊃ (f ∧ f1) ⌢ g | BfAndChopImport |
Proof:
1 | f ⊃ (f1 ⊃ f ∧ f1) | |
2 | f ⊃ (f1 ⊃ f ∧ f1) | |
3 | (f1 ⊃ f ∧ f1) ⊃ (f1 ⌢ g) ⊃ (f ∧ f1) ⌢ g | |
4 | f ∧ (f1 ⌢ g) ⊃ (f ∧ f1) ⌢ g |
qed