Theorem sps 1583

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

Hypothesis

Ref	Expression
sps.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
sps	⊢ (∀𝑥𝜑 → 𝜓)

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 1557	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 14	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1393

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

This theorem is referenced by:  19.21ht  1627  exim  1645  alexdc  1665  19.2  1684  ax10o  1761  hbae  1764  cbv1h  1792  equvini  1804  equveli  1805  ax10oe  1843  drex1  1844  drsb1  1845  exdistrfor  1846  ax11v2  1866  equs5or  1876  sbequi  1885  drsb2  1887  spsbim  1889  sbcomxyyz  2023  hbsb4t  2064  mopick  2156  eupickbi  2160  ceqsalg  2828  mo2icl  2982  reu6  2992  sbcal  3080  csbie2t  3173  dfss4st  3437  reldisj  3543  dfnfc2  3906  ssopab2  4365  eusvnfb  4546  mosubopt  4786  issref  5114  fv3  5655  fvmptt  5731  fnoprabg  6114  bj-exlimmp  16242  strcollnft  16456