An implication and its reverse are equivalent exactly when both operands
are equivalent. The right hand side resembles that of dfbi2, but
<-> is a weaker operator than /\. Note that an implication and
its reverse can never be simultaneously false, because of pm2.521.
(Contributed by Wolf Lammen, 18-Dec-2023.)
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi \leftrightarrow \psi \rightarrow \varphi) \)
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \)
\( \vdash (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \leftrightarrow \psi \rightarrow \varphi) \)