Theorem sps 1963

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

Hypothesis

Ref	Expression
sps.1	|- ( ph -> ps )

Assertion

Ref	Expression
sps	|- ( A. x ph -> ps )

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 1957	. 2 |- ( A. x ph -> ph )
2		sps.1	. 2 |- ( ph -> ps )
3	1, 2	syl 17	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   A.wal 1450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  2sp  1964  19.2g  1966  axc11r  2040  axc15  2153  ax12v2OLD  2191  equveli  2196  dfsb2  2222  drsb1  2226  drsb2  2227  nfsb4t  2238  sbi1  2241  sbco2  2264  sbco3  2266  sb9  2275  sbal1  2309  eujustALT  2322  2eu6  2407  ralcom2  2941  ceqsalgALT  3059  reu6  3215  sbcal  3305  reldisj  3812  dfnfc2  4208  eusvnfb  4597  nfnid  4629  mosubopt  4699  dfid3  4755  issref  5219  fv3  5892  fvmptt  5980  fnoprabg  6416  wfrlem5  7058  pssnn  7808  kmlem16  8613  nd3  9032  axunndlem1  9038  axunnd  9039  axpowndlem1  9040  axregndlem1  9045  axregndlem2  9046  axacndlem5  9054  fundmpss  30478  frrlem5  30589  nalf  31134  unisym1  31154  bj-axc15v  31428  bj-sbsb  31505  bj-mo3OLD  31515  wl-nfimf1  31928  wl-dral1d  31934  wl-nfs1t  31941  wl-sb8t  31950  wl-sbhbt  31952  wl-equsb4  31955  wl-sbalnae  31962  wl-mo3t  31975  wl-ax11-lem5  31983  wl-ax11-lem8  31986  wl-sbcom3  31989  cotrintab  36292  pm11.57  36809  axc5c4c711toc7  36825  axc11next  36827  pm14.122b  36844  dropab1  36870  dropab2  36871  ax6e2eq  36994