Theorem mtt

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

Conclusion
\( \vdash \neg \varphi \rightarrow (\neg \psi \leftrightarrow \psi \rightarrow \varphi) \)
Proof
l0
biimt
\( \vdash \neg \varphi \rightarrow (\neg \psi \leftrightarrow \neg \varphi \rightarrow \neg \psi) \)
con34b
\( \vdash \psi \rightarrow \varphi \leftrightarrow \neg \varphi \rightarrow \neg \psi \)
bitr4di l0 _