Theorem mpdi

A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)

Hypotheses
mpdi.1
\( \vdash \psi \rightarrow \chi \)
mpdi.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
mpdi.1
l1
a1i _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpdi.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
mpdd l1 _