Theorem sps 2223

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 2221	. 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 2215

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

This theorem is used by:  2sp  2224  19.2g  2226  nfim1  2237  axc16g  2296  drsb2  2302  axc11r  2399  axc15  2453  equvel  2487  sb4a  2511  dfsb1  2512  dfsb2  2524  drsb1  2526  nfsb4t  2530  sbco2  2542  sbco3  2544  sb9  2550  sbal1  2559  sbal2  2560  eujustALT  2599  2eu6  2683  ralcom2  3364  ceqsalgALT  3489  reu6  3687  rexdifi  4100  dfnfc2  4892  nfnid  5344  eusvnfb  5362  mosubopt  5491  dfid3  5557  fv3  6900  fvmptt  7011  fnoprabg  7540  fprlem1  8303  pssnn  9167  frrlem15  9743  kmlem16  10172  nd3  10602  axunndlem1  10608  axunnd  10609  axpowndlem1  10610  axregndlem1  10615  axregndlem2  10616  axacndlem5  10624  axsepg3  35675  axsepg3ALT  35676  axsepg5  35678  axnulg  35679  fundmpss  36354  nalfal  37030  unisym1  37050  axtcond  37105  bj-sbsb  37588  wl-nfimf1  38297  wl-axc11r  38301  wl-dral1d  38302  wl-nfs1t  38308  wl-sb8t  38323  wl-sbhbt  38325  wl-equsb4  38328  wl-sbalnae  38333  wl-2spsbbi  38336  wl-mo3t  38347  cotrintab  44462  pm11.57  45221  axc5c4c711toc7  45236  axc11next  45238  pm14.122b  45255  dropab1  45278  dropab2  45279  ax6e2eq  45388  quantgodelALT  47711