Theorem sps 2186

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

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

This theorem is referenced by:  2sp  2187  19.2g  2189  nfim1  2200  axc16g  2261  drsb2  2267  axc11r  2374  axc15  2430  equvel  2464  sb4a  2488  dfsb1  2489  dfsb2  2501  drsb1  2503  nfsb4t  2507  sbco2  2519  sbco3  2521  sb9  2527  sbal1  2536  sbal2  2537  eujustALT  2575  2eu6  2660  ralcom2  3385  ceqsalgALT  3526  reu6  3748  sbcal  3868  rexdifi  4173  dfnfc2  4953  nfnid  5393  eusvnfb  5411  mosubopt  5529  dfid3  5596  fv3  6938  fvmptt  7049  fnoprabg  7573  fprlem1  8341  wfrlem5OLD  8369  pssnn  9234  frrlem15  9826  kmlem16  10235  nd3  10658  axunndlem1  10664  axunnd  10665  axpowndlem1  10666  axregndlem1  10671  axregndlem2  10672  axacndlem5  10680  axsepg2  35058  axsepg2ALT  35059  axnulg  35068  fundmpss  35730  nalfal  36369  unisym1  36389  bj-sbsb  36803  wl-nfimf1  37480  wl-axc11r  37484  wl-dral1d  37485  wl-nfs1t  37491  wl-sb8t  37506  wl-sbhbt  37508  wl-equsb4  37511  wl-sbalnae  37516  wl-2spsbbi  37519  wl-mo3t  37530  wl-ax11-lem5  37543  wl-ax11-lem8  37546  cotrintab  43576  pm11.57  44358  axc5c4c711toc7  44373  axc11next  44375  pm14.122b  44392  dropab1  44416  dropab2  44417  ax6e2eq  44528