Theorem bibi1d

Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis
imbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta \leftrightarrow (\chi \leftrightarrow \theta)) \)
Proof
imbid.1
l1
bibi2d _
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \psi \leftrightarrow (\theta \leftrightarrow \chi)) \)
l2
bicom
\( \vdash \psi \leftrightarrow \theta \leftrightarrow (\theta \leftrightarrow \psi) \)
bicom
\( \vdash \chi \leftrightarrow \theta \leftrightarrow (\theta \leftrightarrow \chi) \)
3bitr4g l1 l2 _