Theorem bibi1i

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

Hypothesis
bibi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
bicom
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\chi \leftrightarrow \varphi) \)
bibi2i.1
l2
bibi2i _
\( \vdash \chi \leftrightarrow \varphi \leftrightarrow (\chi \leftrightarrow \psi) \)
bicom
\( \vdash \chi \leftrightarrow \psi \leftrightarrow (\psi \leftrightarrow \chi) \)
3bitri l0 l2 _