Theorem syldan

A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)

Hypotheses
syldan.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
syldan.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
l0
simpl
\( \vdash \varphi \wedge \psi \rightarrow \varphi \)
l1
syldan.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
syldan.2
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
syl2anc l0 l1 _