Theorem bibi2i

Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)

Hypothesis
bibi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \leftrightarrow \varphi \leftrightarrow (\chi \leftrightarrow \psi) \)
Proof
l0
id
\( \vdash (\chi \leftrightarrow \varphi) \rightarrow (\chi \leftrightarrow \varphi) \)
bibi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
l2
bitrdi l0 _
l3
id
\( \vdash (\chi \leftrightarrow \psi) \rightarrow (\chi \leftrightarrow \psi) \)
bibi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
bitr4di l3 _
impbii l2 _