Theorem mpan2d

A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses
mpan2d.1
\( \vdash \varphi \rightarrow \chi \)
mpan2d.2
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
l0
mpan2d.1
\( \vdash \varphi \rightarrow \chi \)
mpan2d.2
expd _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
mpid l0 _