Theorem syl3an3br

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

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