Theorem sps 1590

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 1564	. 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 1400

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

This theorem is referenced by:  19.21ht  1634  exim  1652  alexdc  1672  19.2  1691  ax10o  1767  hbae  1770  cbv1h  1799  equvini  1811  equveli  1812  ax10oe  1850  drex1  1851  drsb1  1852  exdistrfor  1853  ax11v2  1873  equs5or  1883  sbequi  1892  drsb2  1894  spsbim  1896  sbcomxyyz  2032  hbsb4t  2073  mopick  2165  eupickbi  2169  ceqsalg  2850  mo2icl  3005  reu6  3015  sbcal  3103  csbie2t  3196  dfss4st  3464  reldisj  3575  dfnfc2  3948  ssopab2  4413  eusvnfb  4595  mosubopt  4835  issref  5165  fv3  5713  fvmptt  5791  fnoprabg  6179  bj-exlimmp  16711  strcollnft  16924