Theorem syl6an

A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)

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