Theorem syl2anb

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

Hypotheses
syl2anb.1
\( \vdash \varphi \leftrightarrow \psi \)
syl2anb.2
\( \vdash \tau \leftrightarrow \chi \)
syl2anb.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \tau \rightarrow \theta \)
Proof
l0
syl2anb.2
\( \vdash \tau \leftrightarrow \chi \)
l1
syl2anb.1
\( \vdash \varphi \leftrightarrow \psi \)
syl2anb.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
sylanb l1 _
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
sylan2b l0 _