Theorem mp2an

An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Hypotheses
mp2an.1
\( \vdash \varphi \)
mp2an.2
\( \vdash \psi \)
mp2an.3
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \chi \)
Proof
l0
mp2an.2
\( \vdash \psi \)
l1
mp2an.1
\( \vdash \varphi \)
mp2an.3
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
mpan l1 _
\( \vdash \psi \rightarrow \chi \)
ax-mp l0 _