Theorem bibi12i

The equivalence of two equivalences. (Contributed by NM, 26-May-1993.)

Hypotheses
bibi2i.1
\( \vdash \varphi \leftrightarrow \psi \)
bibi12i.2
\( \vdash \chi \leftrightarrow \theta \)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\psi \leftrightarrow \theta) \)
Proof
bibi12i.2
l1
bibi2i _
\( \vdash \varphi \leftrightarrow \chi \leftrightarrow (\varphi \leftrightarrow \theta) \)
bibi2i.1
bibi1i _
\( \vdash \varphi \leftrightarrow \theta \leftrightarrow (\psi \leftrightarrow \theta) \)
bitri l1 _