Theorem mt4i

Description: Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mt4i.1	⊢ 𝜒
2		mt4i.2	⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ 𝜒 ) )
3	1	a1i	⊢ ( 𝜑 → 𝜒 )
4	3 2	mt4d	⊢ ( 𝜑 → 𝜓 )