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