Theorem sylanr1

A syllogism inference. (Contributed by NM, 9-Apr-2005.)

Hypotheses
sylanr1.1
\( \vdash \varphi \rightarrow \chi \)
sylanr1.2
\( \vdash \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
Conclusion
\( \vdash \psi \wedge (\varphi \wedge \theta) \rightarrow \tau \)
Proof
sylanr1.1
l1
anim1i _
\( \vdash \varphi \wedge \theta \rightarrow \chi \wedge \theta \)
sylanr1.2
\( \vdash \psi \wedge (\chi \wedge \theta) \rightarrow \tau \)
sylan2 l1 _