Theorem syl2anbr

A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses
syl2anbr.1
\( \vdash \psi \leftrightarrow \varphi \)
syl2anbr.2
\( \vdash \chi \leftrightarrow \tau \)
syl2anbr.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \tau \rightarrow \theta \)
Proof
l0
syl2anbr.2
\( \vdash \chi \leftrightarrow \tau \)
l1
syl2anbr.1
\( \vdash \psi \leftrightarrow \varphi \)
syl2anbr.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
sylanbr l1 _
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
sylan2br l0 _