Theorem mp2b

A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

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