Theorem biadan

An implication is equivalent to the equivalence of some implied equivalence and some other equivalence involving a conjunction. A utility lemma as illustrated in biadanii and [elelb]. (Contributed by BJ, 4-Mar-2023.) (Proof shortened by Wolf Lammen, 8-Mar-2023.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi)) \)
Proof
l0
pm4.71r
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\varphi \leftrightarrow \psi \wedge \varphi) \)
l1
bicom
\( \vdash \varphi \leftrightarrow \psi \wedge \varphi \leftrightarrow (\psi \wedge \varphi \leftrightarrow \varphi) \)
l2
bicom
pm5.32
l4
bibi12i l2 _
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \leftrightarrow \psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\psi \wedge \chi \leftrightarrow \varphi \leftrightarrow (\psi \wedge \varphi \leftrightarrow \psi \wedge \chi)) \)
l5
bicom
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi \leftrightarrow \psi \rightarrow (\varphi \leftrightarrow \chi)) \)
biluk
\( \vdash \psi \wedge \varphi \leftrightarrow \varphi \leftrightarrow (\psi \wedge \chi \leftrightarrow \varphi \leftrightarrow (\psi \wedge \varphi \leftrightarrow \psi \wedge \chi)) \)
3bitr4ri l4 l5 _
\( \vdash \psi \wedge \varphi \leftrightarrow \varphi \leftrightarrow (\psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi)) \)
3bitri l0 l1 _