Theorem bitr4i

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

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