Theorem imbitrrdi

A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses
imbitrrdi.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
imbitrrdi.2
\( \vdash \theta \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
l0
imbitrrdi.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
imbitrrdi.2
biimpri _
\( \vdash \chi \rightarrow \theta \)
syl6 l0 _