Theorem syl7bi

A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 14-May-1993.)

Hypotheses
syl7bi.1
\( \vdash \varphi \leftrightarrow \psi \)
syl7bi.2
\( \vdash \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
Conclusion
\( \vdash \chi \rightarrow \theta \rightarrow \varphi \rightarrow \tau \)
Proof
syl7bi.1
l1
biimpi _
\( \vdash \varphi \rightarrow \psi \)
syl7bi.2
\( \vdash \chi \rightarrow \theta \rightarrow \psi \rightarrow \tau \)
syl7 l1 _