Theorem sps 1517

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 1491	. 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 1333

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

This theorem is referenced by:  19.21ht  1561  exim  1579  alexdc  1599  19.2  1618  ax10o  1695  hbae  1698  cbv1h  1726  equvini  1738  equveli  1739  ax10oe  1777  drex1  1778  drsb1  1779  exdistrfor  1780  ax11v2  1800  equs5or  1810  sbequi  1819  drsb2  1821  spsbim  1823  sbcomxyyz  1952  hbsb4t  1993  mopick  2084  eupickbi  2088  ceqsalg  2740  mo2icl  2891  reu6  2901  sbcal  2988  csbie2t  3079  dfss4st  3340  reldisj  3445  dfnfc2  3790  ssopab2  4234  eusvnfb  4412  mosubopt  4648  issref  4965  fv3  5488  fvmptt  5556  fnoprabg  5916  bj-exlimmp  13302  strcollnft  13518