Theorem mpd

A modus ponens deduction. A translation of natural deduction rule -> E ( -> elimination), see [natded]. Deduction form of [ax-mp]. Inference associated with a2i. Commuted form of mpcom. (Contributed by NM, 29-Dec-1992.)

Hypotheses
mpd.1
\( \vdash \varphi \rightarrow \psi \)
mpd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
mpd.1
\( \vdash \varphi \rightarrow \psi \)
mpd.2
a2i _
\( \vdash (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _