Theorem sps 1551

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

Syntax hints:   → wi 4  ∀wal 1362

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

This theorem is referenced by:  19.21ht  1595  exim  1613  alexdc  1633  19.2  1652  ax10o  1729  hbae  1732  cbv1h  1760  equvini  1772  equveli  1773  ax10oe  1811  drex1  1812  drsb1  1813  exdistrfor  1814  ax11v2  1834  equs5or  1844  sbequi  1853  drsb2  1855  spsbim  1857  sbcomxyyz  1991  hbsb4t  2032  mopick  2123  eupickbi  2127  ceqsalg  2791  mo2icl  2943  reu6  2953  sbcal  3041  csbie2t  3133  dfss4st  3396  reldisj  3502  dfnfc2  3857  ssopab2  4310  eusvnfb  4489  mosubopt  4728  issref  5052  fv3  5581  fvmptt  5653  fnoprabg  6023  bj-exlimmp  15415  strcollnft  15630