Theorem a1ddd

Triple deduction introducing an antecedent to a wff. Deduction associated with a1dd. Double deduction associated with a1d. Triple deduction associated with [ax-1] and a1i. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypothesis
a1ddd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \)
Proof
l0
a1ddd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \tau \)
ax-1
\( \vdash \tau \rightarrow \theta \rightarrow \tau \)
syl8 l0 _