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