⊢ | (f ⊃ g) ⊃ f ⊃ g | NextImpDist |
Proof:
1 | ⊢ ¬(f ⊃ g) ≡ f ∧¬g | |
2 | ⊢ skip ; ¬(f ⊃ g) ≡skip ; (f ∧¬g) | |
3 | ⊢ f ⊃ g ∨ (f ∧¬g) | |
4 | ⊢ skip ; f ⊃ (skip ; g) ∨ (skip ; (f ∧¬g)) | |
5 | ⊢ ¬(skip ; (f ∧¬g)) ⊃ (skip ; f) ⊃ (skip ; g) | |
6 | ⊢ ¬(skip ; ¬(f ⊃ g)) ⊃ (skip ; f) ⊃ (skip ; g) | |
7 | ⊢ ¬¬(f ⊃ g) ⊃ f ⊃ g | 6, def. of |
8 | ⊢ (f ⊃ g) ⊃¬¬(f ⊃ g) | |
9 | ⊢ (f ⊃ g) ⊃ f ⊃ g |
qed