Theorem bitr2i

An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)

Hypotheses
bitr2i.1
\( \vdash \varphi \leftrightarrow \psi \)
bitr2i.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \chi \leftrightarrow \varphi \)
Proof
l0
bitr2i.1
\( \vdash \varphi \leftrightarrow \psi \)
bitr2i.2
\( \vdash \psi \leftrightarrow \chi \)
bitri l0 _
bicomi _