Theorem spsd

Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)

Hypothesis
spsd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \psi \rightarrow \chi \)
Proof
l0
sp
\( \vdash \forall x \, \psi \rightarrow \psi \)
spsd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syl5 l0 _