| ⊢ | f ⊃ f | DiIntro |
Proof:
1 | ⊢ f ; empty ≡ f | |
2 | ⊢ empty ⊃true | |
3 | ⊢ (empty ⊃ true) | |
4 | ⊢ (empty ⊃ true) ⊃ (f ; empty ⊃ f ; true) | |
5 | ⊢ f ; empty ⊃ f ; true | |
6 | ⊢ f ; empty ⊃ f | 5, def. of |
7 | ⊢ f ⊃ f |
qed
The following is a corollary of DiIntro: