Theorem syl3an3b

A syllogism inference. (Contributed by NM, 22-Aug-1995.)

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