Theorem imim1d

Deduction adding nested consequents. Deduction associated with imim1 and imim1i. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)

Hypothesis
imim1d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \rightarrow \theta) \rightarrow \psi \rightarrow \theta \)
Proof
l0
imim1d.1
idd
imim12d l0 _