Theorem mpanl12

An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses
mpanl12.1
\( \vdash \varphi \)
mpanl12.2
\( \vdash \psi \)
mpanl12.3
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \chi \rightarrow \theta \)
Proof
l0
mpanl12.2
\( \vdash \psi \)
l1
mpanl12.1
\( \vdash \varphi \)
mpanl12.3
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mpanl1 l1 _
\( \vdash \psi \wedge \chi \rightarrow \theta \)
mpan l0 _