Theorem sps 2055

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 2053	. 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 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2sp  2056  19.2g  2058  nfim1  2067  axc16g  2134  axc11rvOLD  2140  axc11r  2187  axc15  2303  ax12v2OLD  2342  equvel  2347  dfsb2  2373  drsb1  2377  drsb2  2378  nfsb4t  2389  sbi1  2392  sbco2  2415  sbco3  2417  sb9  2426  sbal1  2460  eujustALT  2473  2eu6  2558  ralcom2  3104  ceqsalgALT  3231  reu6  3395  sbcal  3485  reldisj  4020  dfnfc2  4454  dfnfc2OLD  4455  eusvnfb  4862  nfnid  4897  mosubopt  4972  dfid3  5025  issref  5509  fv3  6206  fvmptt  6300  fnoprabg  6761  wfrlem5  7419  pssnn  8178  kmlem16  8987  nd3  9411  axunndlem1  9417  axunnd  9418  axpowndlem1  9419  axregndlem1  9424  axregndlem2  9425  axacndlem5  9433  fundmpss  31664  frrlem5  31784  nalf  32402  unisym1  32422  bj-sbsb  32824  bj-mo3OLD  32832  bj-ax9  32890  wl-nfimf1  33313  wl-dral1d  33318  wl-nfs1t  33324  wl-sb8t  33333  wl-sbhbt  33335  wl-equsb4  33338  wl-sbalnae  33345  wl-mo3t  33358  wl-ax11-lem5  33366  wl-ax11-lem8  33369  wl-sbcom3  33372  cotrintab  37921  pm11.57  38589  axc5c4c711toc7  38605  axc11next  38607  pm14.122b  38624  dropab1  38651  dropab2  38652  ax6e2eq  38773