Theorem sps 2174

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

Hypothesis

Ref	Expression
sps.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
sps	⊢ (∀𝑥𝜑 → 𝜓)

Proof of Theorem sps

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

Syntax hints:   → wi 4  ∀wal 1532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2167

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  2sp  2175  19.2g  2177  nfim1  2188  axc16g  2247  drsb2  2253  axc11r  2361  axc15  2417  equvel  2451  sb4a  2475  dfsb1  2476  dfsb2  2488  drsb1  2490  nfsb4t  2494  sbco2  2506  sbco3  2508  sb9  2514  sbal1  2523  sbal2  2524  eujustALT  2562  2eu6  2648  ralcom2  3370  ceqsalgALT  3506  reu6  3721  sbcal  3840  rexdifi  4144  reldisjOLD  4453  dfnfc2  4932  nfnid  5375  eusvnfb  5393  mosubopt  5512  dfid3  5579  fv3  6915  fvmptt  7025  fnoprabg  7543  fprlem1  8305  wfrlem5OLD  8333  pssnn  9192  pssnnOLD  9289  frrlem15  9780  kmlem16  10188  nd3  10612  axunndlem1  10618  axunnd  10619  axpowndlem1  10620  axregndlem1  10625  axregndlem2  10626  axacndlem5  10634  fundmpss  35362  nalfal  35887  unisym1  35907  bj-sbsb  36314  wl-nfimf1  36993  wl-axc11r  36997  wl-dral1d  36998  wl-nfs1t  37004  wl-sb8t  37019  wl-sbhbt  37021  wl-equsb4  37024  wl-sbalnae  37029  wl-2spsbbi  37032  wl-mo3t  37043  wl-ax11-lem5  37056  wl-ax11-lem8  37059  cotrintab  43044  pm11.57  43826  axc5c4c711toc7  43841  axc11next  43843  pm14.122b  43860  dropab1  43884  dropab2  43885  ax6e2eq  43996