Theorem mpii

A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 31-Jul-2012.)

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