Theorem sps 2222

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2sp  2223  19.2g  2225  nfim1  2236  axc16g  2295  drsb2  2301  axc11r  2398  axc15  2452  equvel  2486  sb4a  2510  dfsb1  2511  dfsb2  2523  drsb1  2525  nfsb4t  2529  sbco2  2541  sbco3  2543  sb9  2549  sbal1  2558  sbal2  2559  eujustALT  2598  2eu6  2682  ralcom2  3363  ceqsalgALT  3487  reu6  3684  rexdifi  4097  dfnfc2  4889  nfnid  5337  eusvnfb  5355  mosubopt  5482  mosubott  5484  dfid3  5549  fv3  6895  fvmptt  7006  fnoprabg  7535  fprlem1  8302  pssnn  9168  frrlem15  9745  kmlem16  10225  nd3  10655  axunndlem1  10661  axunnd  10662  axpowndlem1  10663  axregndlem1  10668  axregndlem2  10669  axacndlem5  10677  axsepg3  35782  axsepg3ALT  35783  axsepg5  35785  axnulg  35786  fundmpss  36501  nalfal  37161  unisym1  37181  axtcond  37236  bj-sbsb  37719  wl-nfimf1  38426  wl-axc11r  38430  wl-dral1d  38431  wl-nfs1t  38437  wl-sb8t  38452  wl-sbhbt  38454  wl-equsb4  38457  wl-sbalnae  38462  wl-2spsbbi  38465  wl-mo3t  38476  cotrintab  44573  pm11.57  45332  axc5c4c711toc7  45347  axc11next  45349  pm14.122b  45366  dropab1  45389  dropab2  45390  ax6e2eq  45499  quantgodelALT  47829