Theorem syl3an1b

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

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