Theorem ibibr

Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow (\psi \leftrightarrow \varphi) \)
Proof
l0
pm5.501
\( \vdash \varphi \rightarrow (\psi \leftrightarrow (\varphi \leftrightarrow \psi)) \)
bicom
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\psi \leftrightarrow \varphi) \)
bitrdi l0 _
pm5.74i _