| ⊢ f ⊃ f | BfImpDf |
Proof:
1 | f ⊃ (empty ⊃ f) | |
2 | f ⊃ (empty ⊃ f) | |
3 | (empty ⊃ f) ⊃ ( empty ⊃ f) | |
4 | f ⊃ ( empty ⊃ f) | |
5 | empty | |
6 | f ⊃ f |
qed