Theorem sps 1917

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 1911	. 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 1436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-12 1906

This theorem depends on definitions:  df-bi 189  df-ex 1661

This theorem is referenced by:  2sp  1918  19.2g  1920  axc112  1994  ax12v2  2139  equveli  2144  dfsb2  2168  drsb1  2172  drsb2  2173  nfsb4t  2184  sbi1  2187  sbco2  2210  sbco3  2212  sb9  2221  sbal1  2256  eujustALT  2269  2eu6  2357  ralcom2  2994  ceqsalgALT  3108  reu6  3261  sbcal  3350  reldisj  3837  dfnfc2  4235  eusvnfb  4618  nfnid  4648  mosubopt  4716  dfid3  4767  issref  5230  fv3  5892  fvmptt  5979  fnoprabg  6409  wfrlem5  7046  pssnn  7794  kmlem16  8597  nd3  9016  axunndlem1  9022  axunnd  9023  axpowndlem1  9024  axregndlem1  9029  axregndlem2  9030  axacndlem5  9038  fundmpss  30408  frrlem5  30519  nalf  31062  unisym1  31082  bj-axc15v  31323  bj-mo3OLD  31411  wl-nfimf1  31816  wl-dral1d  31822  wl-nfs1t  31829  wl-sb8t  31838  wl-sbhbt  31840  wl-equsb4  31843  wl-sbalnae  31850  wl-mo3t  31863  wl-ax12v3  31870  wl-ax11-lem5  31877  wl-ax11-lem8  31880  wl-sbcom3  31883  pm11.57  36641  axc5c4c711toc7  36657  axc11next  36659  pm14.122b  36676  dropab1  36702  dropab2  36703  ax6e2eq  36826