Theorem bitri
An inference from transitive law for logical equivalence. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypotheses
bitri.1
\( \vdash \varphi \leftrightarrow \psi \)
bitri.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \leftrightarrow \chi \)
Proof
l0
bitri.1
l1
biimpi _
l2
bitri.2
l3
sylib l1 _
l4
bitri.2
l5
biimpri _
l6
bitri.1
l7
sylibr l5 _
l8
impbii l3 _