Theorem con4i

Description: Inference associated with con4 . Its associated inference is mt4 .

Remark: this can also be proved using notnot followed by nsyl2 , giving a shorter proof but depending on more axioms (namely, ax-1 and ax-2 ). (Contributed by NM, 29-Dec-1992)

	Ref	Expression
Hypothesis	con4i.1	⊢ ( ¬ 𝜑 → ¬ 𝜓 )
Assertion	con4i	⊢ ( 𝜓 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		con4i.1	⊢ ( ¬ 𝜑 → ¬ 𝜓 )
2		con4	⊢ ( ( ¬ 𝜑 → ¬ 𝜓 ) → ( 𝜓 → 𝜑 ) )
3	1 2	ax-mp	⊢ ( 𝜓 → 𝜑 )