Theorem sps 1943

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 1937	. 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 1442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664

This theorem is referenced by:  2sp  1944  19.2g  1946  axc112  2020  ax12v2  2175  equveli  2180  dfsb2  2202  drsb1  2206  drsb2  2207  nfsb4t  2218  sbi1  2221  sbco2  2244  sbco3  2246  sb9  2255  sbal1  2289  eujustALT  2302  2eu6  2387  ralcom2  2955  ceqsalgALT  3073  reu6  3227  sbcal  3317  reldisj  3808  dfnfc2  4216  eusvnfb  4599  nfnid  4629  mosubopt  4699  dfid3  4750  issref  5213  fv3  5878  fvmptt  5965  fnoprabg  6397  wfrlem5  7040  pssnn  7790  kmlem16  8595  nd3  9014  axunndlem1  9020  axunnd  9021  axpowndlem1  9022  axregndlem1  9027  axregndlem2  9028  axacndlem5  9036  fundmpss  30407  frrlem5  30518  nalf  31063  unisym1  31083  bj-axc15v  31362  bj-mo3OLD  31447  wl-nfimf1  31858  wl-dral1d  31864  wl-nfs1t  31871  wl-sb8t  31880  wl-sbhbt  31882  wl-equsb4  31885  wl-sbalnae  31892  wl-mo3t  31905  wl-ax12v3  31912  wl-ax11-lem5  31919  wl-ax11-lem8  31922  wl-sbcom3  31925  cotrintab  36221  pm11.57  36739  axc5c4c711toc7  36755  axc11next  36757  pm14.122b  36774  dropab1  36800  dropab2  36801  ax6e2eq  36924