Theorem biimpr

Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \psi \rightarrow \varphi \)
Proof
l0
dfbi1
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \)
simprim
\( \vdash \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \rightarrow \psi \rightarrow \varphi \)
sylbi l0 _