Theorem biantr

A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \wedge (\chi \leftrightarrow \psi) \rightarrow (\varphi \leftrightarrow \chi) \)
Proof
id
bibi2d _
biimparc _