| ⊢ | f ⊃ g ⇒ ⊢ f ⊃ g | BoxImpBoxRule |
Proof:
1 | ⊢ f ⊃ g | given |
2 | ⊢ ¬g ⊃¬f | |
3 | ⊢ (¬g ⊃ ¬f) | |
4 | ⊢ (¬g ⊃ ¬f) ⊃ (true ; ¬g) ⊃ (true ; ¬f) | |
5 | ⊢ true ; ¬g ⊃true ; ¬f | |
6 | ⊢ ¬g ⊃¬f | 5, def. of |
7 | ⊢ ¬¬f ⊃¬¬g | |
8 | ⊢ f ⊃ g | 7, def. of |
qed