| ⊢ | (f ⊃ g) ⊃ f ⊃ g | FBoxImpDist |
Proof:
1 | (f ⊃ g) ⊃ (¬g ⊃ ¬f) | |
2 | ¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g) | |
3 | (¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g)) | |
4 | (¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g)) |
|
⊃ (f ⊃ g) ⊃ (¬g ⊃ ¬f) | ||
5 | (f ⊃ g) ⊃ (¬g ⊃ ¬f) | |
6 | (¬g ⊃ ¬f) ⊃ f ⊃ g | |
7 | (f ⊃ g) ⊃ f ⊃ g |
qed