⊢ | (f ⊃ g) ⊃ ( f) ⊃ ( g) | BiImpDist |
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