Theorem 3imtr4i

A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.)

Hypotheses
3imtr4.1
\( \vdash \varphi \rightarrow \psi \)
3imtr4.2
\( \vdash \chi \leftrightarrow \varphi \)
3imtr4.3
\( \vdash \theta \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \rightarrow \theta \)
Proof
l0
3imtr4.2
\( \vdash \chi \leftrightarrow \varphi \)
3imtr4.1
\( \vdash \varphi \rightarrow \psi \)
l2
sylbi l0 _
\( \vdash \chi \rightarrow \psi \)
3imtr4.3
\( \vdash \theta \leftrightarrow \psi \)
sylibr l2 _