Theorem sps 1559

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 1533	. 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 1370

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

This theorem is referenced by:  19.21ht  1603  exim  1621  alexdc  1641  19.2  1660  ax10o  1737  hbae  1740  cbv1h  1768  equvini  1780  equveli  1781  ax10oe  1819  drex1  1820  drsb1  1821  exdistrfor  1822  ax11v2  1842  equs5or  1852  sbequi  1861  drsb2  1863  spsbim  1865  sbcomxyyz  1999  hbsb4t  2040  mopick  2131  eupickbi  2135  ceqsalg  2799  mo2icl  2951  reu6  2961  sbcal  3049  csbie2t  3141  dfss4st  3405  reldisj  3511  dfnfc2  3867  ssopab2  4321  eusvnfb  4500  mosubopt  4739  issref  5064  fv3  5598  fvmptt  5670  fnoprabg  6045  bj-exlimmp  15667  strcollnft  15882