Theorem sps

Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)

Hypothesis
sps.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
sp
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
sps.1
\( \vdash \varphi \rightarrow \psi \)
syl l0 _