Theorem syl3an2b

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

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