Theorem sylanr2

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

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