Theorem sps 1427

Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sps.1	|- (ph -> ps)

Assertion

Ref	Expression
sps	|- (A.xph -> ps)

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 1398	. 2 |- (A.xph -> ph)
2		sps.1	. 2 |- (ph -> ps)
3	1, 2	syl 14	1 |- (A.xph -> ps)

Syntax hints:   -> wi 4  A.wal 1240

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

This theorem is referenced by:  19.21ht  1470  exim  1487  alexdc  1507  19.2  1526  ax10o  1600  hbae  1603  cbv1h  1630  equvini  1638  equveli  1639  ax10oe  1675  drex1  1676  drsb1  1677  exdistrfor  1678  ax11v2  1698  equs5or  1708  sbequi  1717  drsb2  1719  spsbim  1721  sbcomxyyz  1843  hbsb4t  1886  mopick  1975  eupickbi  1979  ceqsalg  2576  mo2icl  2714  reu6  2724  sbcal  2804  csbie2t  2888  reldisj  3265  dfnfc2  3589  ssopab2  4003  eusvnfb  4152  mosubopt  4348  issref  4650  fv3  5140  fvmptt  5205  fnoprabg  5544  bj-exlimmp  9244  strcollnft  9444