| ⊢ | f ⊃ f ∧ f | BoxImpNowAndWeakNext |
Proof:
1 | ⊢ ¬f ⊃¬f | |
2 | ⊢ ¬¬f ⊃ f | |
3 | ⊢ f ⊃ f | 2, def. of |
4 | ⊢ ¬f ⊃¬f | |
5 | ⊢ ¬¬¬f ⊃¬f | |
6 | ⊢ ¬¬¬f ⊃¬f | |
7 | ⊢ ¬¬¬f ⊃¬f | |
8 | ⊢ ¬ f ⊃¬f | 7, def. of |
9 | ⊢ ¬¬f ⊃¬¬ f | |
10 | ⊢ f ⊃ f | 9, def. of , |
11 | ⊢ f ⊃ f ∧ f |
qed