Theorem nsyl4

Description: A negated syllogism inference. (Contributed by NM, 15-Feb-1996)

	Ref	Expression
Hypotheses	nsyl4.1	|- ( ph -> ps )
	nsyl4.2	|- ( -. ph -> ch )
Assertion	nsyl4	|- ( -. ch -> ps )

Proof

Step	Hyp	Ref	Expression
1		nsyl4.1	|- ( ph -> ps )
2		nsyl4.2	|- ( -. ph -> ch )
3	2	con1i	|- ( -. ch -> ph )
4	3 1	syl	|- ( -. ch -> ps )