⊢ | f ⊃ f | BaElim |
Proof:
1 | ⊢ f ≡ f | |
1 | ⊢ f ⊃ f | |
2 | ⊢ ( f ⊃ f) | |
3 | ⊢ ( f ⊃ f) ⊃ f ⊃ f | |
4 | ⊢ f ⊃ f | |
5 | ⊢ f ⊃ f | |
6 | ⊢ f ⊃ f |
qed
Here is a corollary: