Theorem sps 2187

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2179

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  2sp  2188  19.2g  2190  nfim1  2201  axc16g  2262  drsb2  2268  axc11r  2367  axc15  2421  equvel  2455  sb4a  2479  dfsb1  2480  dfsb2  2492  drsb1  2494  nfsb4t  2498  sbco2  2510  sbco3  2512  sb9  2518  sbal1  2527  sbal2  2528  eujustALT  2566  2eu6  2651  ralcom2  3341  ceqsalgALT  3471  reu6  3683  rexdifi  4098  dfnfc2  4879  nfnid  5311  eusvnfb  5329  mosubopt  5448  dfid3  5512  fv3  6835  fvmptt  6944  fnoprabg  7464  fprlem1  8225  pssnn  9073  frrlem15  9642  kmlem16  10049  nd3  10472  axunndlem1  10478  axunnd  10479  axpowndlem1  10480  axregndlem1  10485  axregndlem2  10486  axacndlem5  10494  axsepg2  35084  axsepg2ALT  35085  axnulg  35094  fundmpss  35779  nalfal  36416  unisym1  36436  bj-sbsb  36850  wl-nfimf1  37539  wl-axc11r  37543  wl-dral1d  37544  wl-nfs1t  37550  wl-sb8t  37565  wl-sbhbt  37567  wl-equsb4  37570  wl-sbalnae  37575  wl-2spsbbi  37578  wl-mo3t  37589  wl-ax11-lem5  37602  wl-ax11-lem8  37605  cotrintab  43626  pm11.57  44401  axc5c4c711toc7  44416  axc11next  44418  pm14.122b  44435  dropab1  44458  dropab2  44459  ax6e2eq  44569