Metamath Proof Explorer


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 ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜓𝜑 ) ) )