Theorem a1d

Deduction introducing an embedded antecedent. Deduction form of [ax-1] and a1i. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

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