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	|- ( -. ph -> -. ps )
Assertion	con4i	|- ( ps -> ph )

Proof

Step	Hyp	Ref	Expression
1		con4i.1	|- ( -. ph -> -. ps )
2		con4	|- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
3	1 2	ax-mp	|- ( ps -> ph )