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 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  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  3684  rexdifi  4097  dfnfc2  4889  nfnid  5340  eusvnfb  5358  mosubopt  5487  dfid3  5553  fv3  6897  fvmptt  7008  fnoprabg  7537  fprlem1  8300  pssnn  9164  frrlem15  9740  kmlem16  10169  nd3  10599  axunndlem1  10605  axunnd  10606  axpowndlem1  10607  axregndlem1  10612  axregndlem2  10613  axacndlem5  10621  axsepg3  35668  axsepg3ALT  35669  axsepg5  35671  axnulg  35672  fundmpss  36347  nalfal  37023  unisym1  37043  axtcond  37098  bj-sbsb  37581  wl-nfimf1  38290  wl-axc11r  38294  wl-dral1d  38295  wl-nfs1t  38301  wl-sb8t  38316  wl-sbhbt  38318  wl-equsb4  38321  wl-sbalnae  38326  wl-2spsbbi  38329  wl-mo3t  38340  cotrintab  44455  pm11.57  45214  axc5c4c711toc7  45229  axc11next  45231  pm14.122b  45248  dropab1  45271  dropab2  45272  ax6e2eq  45381  quantgodelALT  47704