Theorem sps 1560

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 1534	. 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 1371

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

This theorem is referenced by:  19.21ht  1604  exim  1622  alexdc  1642  19.2  1661  ax10o  1738  hbae  1741  cbv1h  1769  equvini  1781  equveli  1782  ax10oe  1820  drex1  1821  drsb1  1822  exdistrfor  1823  ax11v2  1843  equs5or  1853  sbequi  1862  drsb2  1864  spsbim  1866  sbcomxyyz  2000  hbsb4t  2041  mopick  2132  eupickbi  2136  ceqsalg  2800  mo2icl  2952  reu6  2962  sbcal  3050  csbie2t  3142  dfss4st  3406  reldisj  3512  dfnfc2  3868  ssopab2  4322  eusvnfb  4501  mosubopt  4740  issref  5065  fv3  5599  fvmptt  5671  fnoprabg  6046  bj-exlimmp  15705  strcollnft  15920