Theorem sps 1802

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 1796	. 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 1368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794

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

This theorem is referenced by:  2sp  1803  19.2g  1805  axc112  1872  cbv1hOLD  1972  ax12v2  2040  equveli  2045  dfsb2  2071  drsb1  2075  drsb2  2076  nfsb4t  2087  sbnOLD  2090  sbi1  2091  sbco2  2118  sbco2OLD  2119  sbco3  2121  sb9  2133  sbcom2OLD  2159  sbal1  2178  sbal1OLD  2179  eujustALT  2263  mo3OLD  2306  eupickbiOLD  2354  2eu6  2378  ralcom2  2983  ceqsalgALT  3096  reu6  3247  sbcal  3338  reldisj  3822  dfnfc2  4209  eusvnfb  4588  nfnid  4621  mosubopt  4689  dfid3  4737  issref  5311  fv3  5804  fvmptt  5890  fnoprabg  6293  pssnn  7634  kmlem16  8437  nd3  8856  axunndlem1  8862  axunnd  8863  axpowndlem1  8864  axpowndlem3OLD  8868  axregndlem1  8871  axregndlem2  8872  axregndOLD  8874  axacndlem5  8881  bwthOLD  19132  fundmpss  27713  wfrlem5  27864  frrlem5  27908  nalf  28385  unisym1  28405  wl-nfimf1  28494  wl-dral1d  28500  wl-nfs1t  28507  wl-sb8t  28516  wl-sbhbt  28518  wl-equsb4  28521  wl-sbalnae  28528  wl-mo3t  28537  wl-ax11-lem5  28545  wl-ax11-lem8  28548  wl-sbcom3  28551  pm11.57  29782  axc5c4c711toc7  29798  axc11next  29800  pm14.122b  29817  dropab1  29843  dropab2  29844  ax6e2eq  31568  bj-axc15v  32567