Theorem mpi

A nested modus ponens inference. Inference associated with com12. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Hypotheses
mpi.1
\( \vdash \psi \)
mpi.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
mpi.1
l1
a1i _
\( \vdash \varphi \rightarrow \psi \)
mpi.2
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpd l1 _