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

Proof

Step	Hyp	Ref	Expression
1		mt3.1	$$⊢\neg \psi$$
2		mt3.2	$$⊢\neg \phi \to \psi$$
3	1 2	mto	$$⊢\neg \neg \phi$$
4	3	notnotri	$$⊢\phi$$