Theorem bitr3i

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

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