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  2766  mo2icl  2917  reu6  2927  sbcal  3015  csbie2t  3106  dfss4st  3369  reldisj  3475  dfnfc2  3828  ssopab2  4276  eusvnfb  4455  mosubopt  4692  issref  5012  fv3  5539  fvmptt  5608  fnoprabg  5976  bj-exlimmp  14524  strcollnft  14739