Theorem sps 2225

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 2223	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  2sp  2226  19.2g  2228  nfim1  2239  axc16g  2298  drsb2  2304  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  3490  reu6  3687  rexdifi  4089  dfnfc2  4892  nfnid  5342  eusvnfb  5360  mosubopt  5487  mosubott  5489  dfid3  5554  fv3  6929  fvmptt  7040  fnoprabg  7569  fprlem1  8349  pssnn  9215  frrlem15  9791  kmlem16  10274  nd3  10704  axunndlem1  10710  axunnd  10711  axpowndlem1  10712  axregndlem1  10717  axregndlem2  10718  axacndlem5  10726  reu6f  35792  axsepg3  35922  axsepg3ALT  35923  axsepg5  35925  axnulg  35926  onprcf1acwevdlem1  36058  fundmpss  36723  nalfal  37382  unisym1  37402  axtcond  37457  bj-sbsb  37940  wl-nfimf1  38663  wl-axc11r  38667  wl-dral1d  38668  wl-nfs1t  38674  wl-sb8t  38689  wl-sbhbt  38691  wl-equsb4  38694  wl-sbalnae  38699  wl-2spsbbi  38702  wl-mo3t  38713  cotrintab  44817  pm11.57  45576  axc5c4c711toc7  45591  axc11next  45593  pm14.122b  45609  dropab1  45632  dropab2  45633  ax6e2eq  45742  quantgodelALT  48100