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 ⊢ (∀𝑥𝜑 → 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  2sp  2222  19.2g  2224  nfim1  2235  axc16g  2294  drsb2  2300  axc11r  2397  axc15  2451  equvel  2485  sb4a  2509  dfsb1  2510  dfsb2  2522  drsb1  2524  nfsb4t  2528  sbco2  2540  sbco3  2542  sb9  2548  sbal1  2557  sbal2  2558  eujustALT  2597  2eu6  2681  ralcom2  3362  ceqsalgALT  3486  reu6  3683  rexdifi  4086  dfnfc2  4888  nfnid  5336  eusvnfb  5354  mosubopt  5481  mosubott  5483  dfid3  5548  fv3  6903  fvmptt  7014  fnoprabg  7543  fprlem1  8321  pssnn  9187  frrlem15  9764  kmlem16  10247  nd3  10677  axunndlem1  10683  axunnd  10684  axpowndlem1  10685  axregndlem1  10690  axregndlem2  10691  axacndlem5  10699  reu6f  35755  axsepg3  35865  axsepg3ALT  35866  axsepg5  35868  axnulg  35869  onprcf1acwevdlem1  35964  fundmpss  36624  nalfal  37283  unisym1  37303  axtcond  37358  bj-sbsb  37841  wl-nfimf1  38551  wl-axc11r  38555  wl-dral1d  38556  wl-nfs1t  38562  wl-sb8t  38577  wl-sbhbt  38579  wl-equsb4  38582  wl-sbalnae  38587  wl-2spsbbi  38590  wl-mo3t  38601  cotrintab  44707  pm11.57  45466  axc5c4c711toc7  45481  axc11next  45483  pm14.122b  45500  dropab1  45523  dropab2  45524  ax6e2eq  45633  quantgodelALT  47978