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 )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1563

This theorem is used 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  3576  dfnfc2  3953  ssopab2  4418  eusvnfb  4600  mosubopt  4840  issref  5170  fv3  5718  fvmptt  5797  fnoprabg  6189  bj-exlimmp  16797  strcollnft  17010