Theorem mpid

A nested modus ponens deduction. Deduction associated with mpi. (Contributed by NM, 14-Dec-2004.)

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