Theorem mpanr12

An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses
mpanr12.1
\( \vdash \psi \)
mpanr12.2
\( \vdash \chi \)
mpanr12.3
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
mpanr12.2
\( \vdash \chi \)
l1
mpanr12.1
\( \vdash \psi \)
mpanr12.3
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
mpanr1 l1 _
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
mpan2 l0 _