Theorem sps 1809

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 1803	. 2 |- ( A. x ph -> ph )
2		sps.1	. 2 |- ( ph -> ps )
3	1, 2	syl 16	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   A.wal 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798

This theorem depends on definitions:  df-bi 185  df-ex 1592

This theorem is referenced by:  2sp  1810  19.2g  1812  axc112  1879  cbv1hOLD  1981  ax12v2  2049  equveli  2054  dfsb2  2080  drsb1  2084  drsb2  2085  nfsb4t  2096  sbnOLD  2099  sbi1  2100  sbco2  2127  sbco2OLD  2128  sbco3  2130  sb9  2142  sbcom2OLD  2167  sbal1  2186  sbal1OLD  2187  eujustALT  2271  mo3OLD  2314  eupickbiOLD  2362  2eu6  2386  ralcom2  3019  ceqsalgALT  3132  reu6  3285  sbcal  3376  reldisj  3863  dfnfc2  4256  eusvnfb  4636  nfnid  4669  mosubopt  4738  dfid3  4789  issref  5371  fv3  5870  fvmptt  5956  fnoprabg  6378  pssnn  7728  kmlem16  8534  nd3  8953  axunndlem1  8959  axunnd  8960  axpowndlem1  8961  axpowndlem3OLD  8965  axregndlem1  8968  axregndlem2  8969  axregndOLD  8971  axacndlem5  8978  bwthOLD  19670  fundmpss  28759  wfrlem5  28910  frrlem5  28954  nalf  29431  unisym1  29451  wl-nfimf1  29541  wl-dral1d  29547  wl-nfs1t  29554  wl-sb8t  29563  wl-sbhbt  29565  wl-equsb4  29568  wl-sbalnae  29575  wl-mo3t  29584  wl-ax11-lem5  29592  wl-ax11-lem8  29595  wl-sbcom3  29598  pm11.57  30828  axc5c4c711toc7  30844  axc11next  30846  pm14.122b  30863  dropab1  30889  dropab2  30890  ax6e2eq  32285  bj-axc15v  33286