Theorem pm2.86d

Deduction associated with pm2.86. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)

Hypothesis
pm2.86d.1
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Proof
l0
ax-1
\( \vdash \chi \rightarrow \psi \rightarrow \chi \)
pm2.86d.1
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
syl5 l0 _
com23 _