Theorem sps 1471

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 1442	. 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 1283

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

This theorem is referenced by:  19.21ht  1514  exim  1531  alexdc  1551  19.2  1570  ax10o  1644  hbae  1647  cbv1h  1674  equvini  1682  equveli  1683  ax10oe  1719  drex1  1720  drsb1  1721  exdistrfor  1722  ax11v2  1742  equs5or  1752  sbequi  1761  drsb2  1763  spsbim  1765  sbcomxyyz  1888  hbsb4t  1931  mopick  2020  eupickbi  2024  ceqsalg  2628  mo2icl  2772  reu6  2782  sbcal  2866  csbie2t  2951  reldisj  3302  dfnfc2  3627  ssopab2  4038  eusvnfb  4212  mosubopt  4431  issref  4737  fv3  5229  fvmptt  5294  fnoprabg  5633  bj-exlimmp  10731  strcollnft  10937