Theorem mtt

Description: Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001) (Proof shortened by Wolf Lammen, 12-Nov-2012)

	Ref	Expression
Assertion	mtt	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜓 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		biimt	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( ¬ 𝜑 → ¬ 𝜓 ) ) )
2		con34b	⊢ ( ( 𝜓 → 𝜑 ) ↔ ( ¬ 𝜑 → ¬ 𝜓 ) )
3	1 2	bitr4di	⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜓 → 𝜑 ) ) )