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	$$⊢\neg \phi \to \neg \psi$$
Assertion	con4i	$$⊢\psi \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		con4i.1	$$⊢\neg \phi \to \neg \psi$$
2		con4	$$⊢\left(\neg \phi \to \neg \psi \right)\to \left(\psi \to \phi \right)$$
3	1 2	ax-mp	$$⊢\psi \to \phi$$