Theorem mp2

A double modus ponens inference. (Contributed by NM, 5-Apr-1994.)

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