Theorem syl2and

A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses
syl2and.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl2and.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
syl2and.3
\( \vdash \varphi \rightarrow \chi \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \theta \rightarrow \eta \)
Proof
l0
syl2and.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
syl2and.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
syl2and.3
\( \vdash \varphi \rightarrow \chi \wedge \tau \rightarrow \eta \)
sylan2d l1 _
\( \vdash \varphi \rightarrow \chi \wedge \theta \rightarrow \eta \)
syland l0 _