Theorem sps 1585

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 1559	. 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 1395

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

This theorem is referenced by:  19.21ht  1629  exim  1647  alexdc  1667  19.2  1686  ax10o  1763  hbae  1766  cbv1h  1794  equvini  1806  equveli  1807  ax10oe  1845  drex1  1846  drsb1  1847  exdistrfor  1848  ax11v2  1868  equs5or  1878  sbequi  1887  drsb2  1889  spsbim  1891  sbcomxyyz  2025  hbsb4t  2066  mopick  2158  eupickbi  2162  ceqsalg  2831  mo2icl  2985  reu6  2995  sbcal  3083  csbie2t  3176  dfss4st  3440  reldisj  3546  dfnfc2  3911  ssopab2  4370  eusvnfb  4551  mosubopt  4791  issref  5119  fv3  5662  fvmptt  5738  fnoprabg  6121  bj-exlimmp  16365  strcollnft  16579