Theorem sps 1517

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 1488	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 14	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1329

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

This theorem is referenced by:  19.21ht  1560  exim  1578  alexdc  1598  19.2  1617  ax10o  1693  hbae  1696  cbv1h  1723  equvini  1731  equveli  1732  ax10oe  1769  drex1  1770  drsb1  1771  exdistrfor  1772  ax11v2  1792  equs5or  1802  sbequi  1811  drsb2  1813  spsbim  1815  sbcomxyyz  1945  hbsb4t  1988  mopick  2077  eupickbi  2081  ceqsalg  2714  mo2icl  2863  reu6  2873  sbcal  2960  csbie2t  3048  dfss4st  3309  reldisj  3414  dfnfc2  3754  ssopab2  4197  eusvnfb  4375  mosubopt  4604  issref  4921  fv3  5444  fvmptt  5512  fnoprabg  5872  bj-exlimmp  12976  strcollnft  13182