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	⊢ ¬ 𝜓
	mt3.2	⊢ ( ¬ 𝜑 → 𝜓 )
Assertion	mt3	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		mt3.1	⊢ ¬ 𝜓
2		mt3.2	⊢ ( ¬ 𝜑 → 𝜓 )
3	1 2	mto	⊢ ¬ ¬ 𝜑
4	3	notnotri	⊢ 𝜑