Theorem syldanl

A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.)

Hypotheses
syldanl.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
syldanl.2
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \theta \rightarrow \tau \)
Proof
syldanl.1
ex _
l2
imdistani _
\( \vdash \varphi \wedge \psi \rightarrow \varphi \wedge \chi \)
syldanl.2
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \tau \)
sylan l2 _