Theorem bibi2d

Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis
imbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi \leftrightarrow (\theta \leftrightarrow \chi)) \)
Proof
imbid.1
pm5.74i _
l2
bibi2i _
\( \vdash \varphi \rightarrow \theta \leftrightarrow \varphi \rightarrow \psi \leftrightarrow (\varphi \rightarrow \theta \leftrightarrow \varphi \rightarrow \chi) \)
l3
pm5.74
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi) \leftrightarrow (\varphi \rightarrow \theta \leftrightarrow \varphi \rightarrow \psi) \)
pm5.74
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \chi) \leftrightarrow (\varphi \rightarrow \theta \leftrightarrow \varphi \rightarrow \chi) \)
3bitr4i l2 l3 _
pm5.74ri _