NextImpDist

1	⊢ ¬(f ⊃ g) ≡ f ∧¬g	Prop
2	⊢ skip ; ¬(f ⊃ g) ≡skip ; (f ∧¬g)	1,RightChopEqvChop
3	⊢ f ⊃ g ∨ (f ∧¬g)	Prop
4	⊢ skip ; f ⊃ (skip ; g) ∨ (skip ; (f ∧¬g))	3,ChopOrImpRule
5	⊢ ¬(skip ; (f ∧¬g)) ⊃ (skip ; f) ⊃ (skip ; g)	4,Prop
6	⊢ ¬(skip ; ¬(f ⊃ g)) ⊃ (skip ; f) ⊃ (skip ; g)	2, 5,Prop
7	⊢ ¬¬(f ⊃ g) ⊃ f ⊃ g	6, def. of
8	⊢ (f ⊃ g) ⊃¬¬(f ⊃ g)	NextImpNotNextNot
9	⊢ (f ⊃ g) ⊃ f ⊃ g	7, 8,Prop