Theorem sps 1561

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

This theorem is referenced by:  19.21ht  1605  exim  1623  alexdc  1643  19.2  1662  ax10o  1739  hbae  1742  cbv1h  1770  equvini  1782  equveli  1783  ax10oe  1821  drex1  1822  drsb1  1823  exdistrfor  1824  ax11v2  1844  equs5or  1854  sbequi  1863  drsb2  1865  spsbim  1867  sbcomxyyz  2001  hbsb4t  2042  mopick  2134  eupickbi  2138  ceqsalg  2805  mo2icl  2959  reu6  2969  sbcal  3057  csbie2t  3150  dfss4st  3414  reldisj  3520  dfnfc2  3882  ssopab2  4340  eusvnfb  4519  mosubopt  4758  issref  5084  fv3  5622  fvmptt  5694  fnoprabg  6069  bj-exlimmp  15905  strcollnft  16119