Theorem mt3

Description: A rule similar to modus tollens. Inference associated with con1i . (Contributed by NM, 18-May-1994) (Proof shortened by Wolf Lammen, 11-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mt3.1	|- -. ps
2		mt3.2	|- ( -. ph -> ps )
3	1 2	mto	|- -. -. ph
4	3	notnotri	|- ph