Theorem a2d

Deduction distributing an embedded antecedent. Deduction form of [ax-2]. (Contributed by NM, 23-Jun-1994.)

Hypothesis
a2d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
Proof
l0
a2d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
ax-2
\( \vdash (\psi \rightarrow \chi \rightarrow \theta) \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
syl l0 _