Theorem sps 1537

Description: Generalization of antecedent. (Contributed by NM, 5-Aug-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 1511	. 2 |- ( A. x ph -> ph )
2		sps.1	. 2 |- ( ph -> ps )
3	1, 2	syl 14	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   A.wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1510

This theorem is referenced by:  19.21ht  1581  exim  1599  alexdc  1619  19.2  1638  ax10o  1715  hbae  1718  cbv1h  1746  equvini  1758  equveli  1759  ax10oe  1797  drex1  1798  drsb1  1799  exdistrfor  1800  ax11v2  1820  equs5or  1830  sbequi  1839  drsb2  1841  spsbim  1843  sbcomxyyz  1972  hbsb4t  2013  mopick  2104  eupickbi  2108  ceqsalg  2765  mo2icl  2916  reu6  2926  sbcal  3014  csbie2t  3105  dfss4st  3368  reldisj  3474  dfnfc2  3827  ssopab2  4275  eusvnfb  4454  mosubopt  4691  issref  5011  fv3  5538  fvmptt  5607  fnoprabg  5975  bj-exlimmp  14441  strcollnft  14656