Theorem embantd

Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.)

Hypotheses
embantd.1
\( \vdash \varphi \rightarrow \psi \)
embantd.2
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \theta \)
Proof
l0
embantd.1
\( \vdash \varphi \rightarrow \psi \)
embantd.2
imim2d _
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
mpid l0 _