Theorem mt4

Description: The rule of modus tollens. Inference associated with con4i . (Contributed by Wolf Lammen, 12-May-2013)

	Ref	Expression
Hypotheses	mt4.1	⊢ 𝜑
	mt4.2	⊢ ( ¬ 𝜓 → ¬ 𝜑 )
Assertion	mt4	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		mt4.1	⊢ 𝜑
2		mt4.2	⊢ ( ¬ 𝜓 → ¬ 𝜑 )
3	2	con4i	⊢ ( 𝜑 → 𝜓 )
4	1 3	ax-mp	⊢ 𝜓