Theorem syl3an1br

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

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