Theorem sps 1518

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 1489	. 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 1330

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

This theorem is referenced by:  19.21ht  1561  exim  1579  alexdc  1599  19.2  1618  ax10o  1694  hbae  1697  cbv1h  1724  equvini  1732  equveli  1733  ax10oe  1770  drex1  1771  drsb1  1772  exdistrfor  1773  ax11v2  1793  equs5or  1803  sbequi  1812  drsb2  1814  spsbim  1816  sbcomxyyz  1946  hbsb4t  1989  mopick  2078  eupickbi  2082  ceqsalg  2717  mo2icl  2867  reu6  2877  sbcal  2964  csbie2t  3053  dfss4st  3314  reldisj  3419  dfnfc2  3762  ssopab2  4205  eusvnfb  4383  mosubopt  4612  issref  4929  fv3  5452  fvmptt  5520  fnoprabg  5880  bj-exlimmp  13147  strcollnft  13353