Theorem mpanr1

An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses
mpanr1.1
\( \vdash \psi \)
mpanr1.2
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Proof
l0
mpanr1.1
\( \vdash \psi \)
mpanr1.2
anassrs _
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mpanl2 l0 _