Theorem syl2ani

A syllogism inference. (Contributed by NM, 3-Aug-1999.)

Hypotheses
syl2ani.1
\( \vdash \varphi \rightarrow \chi \)
syl2ani.2
\( \vdash \eta \rightarrow \theta \)
syl2ani.3
\( \vdash \psi \rightarrow \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \psi \rightarrow \varphi \wedge \eta \rightarrow \tau \)
Proof
l0
syl2ani.1
\( \vdash \varphi \rightarrow \chi \)
l1
syl2ani.2
\( \vdash \eta \rightarrow \theta \)
syl2ani.3
\( \vdash \psi \rightarrow \chi \wedge \theta \rightarrow \tau \)
sylan2i l1 _
\( \vdash \psi \rightarrow \chi \wedge \eta \rightarrow \tau \)
sylani l0 _