Theorem sps 1870

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 1864	. 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 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859

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

This theorem is referenced by:  2sp  1871  19.2g  1873  axc112  1942  ax12v2  2087  equveli  2092  dfsb2  2116  drsb1  2120  drsb2  2121  nfsb4t  2132  sbi1  2135  sbco2  2160  sbco3  2162  sb9  2171  sbal1  2206  eujustALT  2287  mo3OLD  2325  2eu6  2380  ralcom2  3019  ceqsalgALT  3132  reu6  3285  sbcal  3374  reldisj  3858  dfnfc2  4253  eusvnfb  4633  nfnid  4666  mosubopt  4734  dfid3  4785  issref  5368  fv3  5861  fvmptt  5947  fnoprabg  6376  pssnn  7731  kmlem16  8536  nd3  8955  axunndlem1  8961  axunnd  8962  axpowndlem1  8963  axregndlem1  8968  axregndlem2  8969  axregndOLD  8971  axacndlem5  8978  fundmpss  29437  wfrlem5  29587  frrlem5  29631  nalf  30096  unisym1  30116  wl-nfimf1  30218  wl-dral1d  30224  wl-nfs1t  30231  wl-sb8t  30240  wl-sbhbt  30242  wl-equsb4  30245  wl-sbalnae  30252  wl-mo3t  30261  wl-ax11-lem5  30269  wl-ax11-lem8  30272  wl-sbcom3  30275  pm11.57  31536  axc5c4c711toc7  31552  axc11next  31554  pm14.122b  31571  dropab1  31597  dropab2  31598  ax6e2eq  33724  bj-axc15v  34731