Theorem mpdd

A nested modus ponens deduction. Double deduction associated with [ax-mp]. Deduction associated with mpd. (Contributed by NM, 12-Dec-2004.)

Hypotheses
mpdd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpdd.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
l0
mpdd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpdd.2
a2d _
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
mpd l0 _