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