Theorem sps 2221

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

Syntax hints:   → wi 4  ∀wal 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  2sp  2222  19.2g  2224  nfim1  2235  axc16g  2296  drsb2  2302  axc11r  2400  axc15  2454  equvel  2488  sb4a  2512  dfsb1  2513  dfsb2  2525  drsb1  2527  nfsb4t  2531  sbco2  2543  sbco3  2545  sb9  2551  sbal1  2560  sbal2  2561  eujustALT  2600  2eu6  2684  ralcom2  3366  ceqsalgALT  3491  reu6  3690  rexdifi  4105  dfnfc2  4895  nfnid  5348  eusvnfb  5366  mosubopt  5495  dfid3  5561  fv3  6901  fvmptt  7012  fnoprabg  7535  fprlem1  8298  pssnn  9154  frrlem15  9730  kmlem16  10150  nd3  10575  axunndlem1  10581  axunnd  10582  axpowndlem1  10583  axregndlem1  10588  axregndlem2  10589  axacndlem5  10597  axsepg3  35532  axsepg3ALT  35533  axsepg5  35535  axnulg  35536  fundmpss  36237  nalfal  36892  unisym1  36912  axtcond  36967  bj-sbsb  37450  wl-nfimf1  38159  wl-axc11r  38163  wl-dral1d  38164  wl-nfs1t  38170  wl-sb8t  38185  wl-sbhbt  38187  wl-equsb4  38190  wl-sbalnae  38195  wl-2spsbbi  38198  wl-mo3t  38209  cotrintab  44320  pm11.57  45079  axc5c4c711toc7  45094  axc11next  45096  pm14.122b  45113  dropab1  45136  dropab2  45137  ax6e2eq  45246  quantgodelALT  47569