Theorem mpanlr1

An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses
mpanlr1.1
\( \vdash \psi \)
mpanlr1.2
\( \vdash \varphi \wedge (\psi \wedge \chi) \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \chi \wedge \theta \rightarrow \tau \)
Proof
mpanlr1.1
l1
jctl _
\( \vdash \chi \rightarrow \psi \wedge \chi \)
mpanlr1.2
\( \vdash \varphi \wedge (\psi \wedge \chi) \wedge \theta \rightarrow \tau \)
sylanl2 l1 _