Theorem a1dd

Double deduction introducing an antecedent. Deduction associated with a1d. Double deduction associated with [ax-1] and a1i. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)

Hypothesis
a1dd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \chi \)
Proof
l0
a1dd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
ax-1
\( \vdash \chi \rightarrow \theta \rightarrow \chi \)
syl6 l0 _