Theorem syl2anr

A double syllogism inference. For an implication-only version, see syl2imc. (Contributed by NM, 17-Sep-2013.)

Hypotheses
syl2an.1
\( \vdash \varphi \rightarrow \psi \)
syl2an.2
\( \vdash \tau \rightarrow \chi \)
syl2an.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \tau \wedge \varphi \rightarrow \theta \)
Proof
l0
syl2an.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl2an.2
\( \vdash \tau \rightarrow \chi \)
syl2an.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
syl2an l0 l1 _
ancoms _