Theorem imbitrdi

A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

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