Theorem syl3an2br

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

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