Theorem 3imtr3i

A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)

Hypotheses
3imtr3.1
\( \vdash \varphi \rightarrow \psi \)
3imtr3.2
\( \vdash \varphi \leftrightarrow \chi \)
3imtr3.3
\( \vdash \psi \leftrightarrow \theta \)
Conclusion
\( \vdash \chi \rightarrow \theta \)
Proof
l0
3imtr3.2
\( \vdash \varphi \leftrightarrow \chi \)
3imtr3.1
\( \vdash \varphi \rightarrow \psi \)
l2
sylbir l0 _
\( \vdash \chi \rightarrow \psi \)
3imtr3.3
\( \vdash \psi \leftrightarrow \theta \)
sylib l2 _