Theorem sps 2224

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 2222	. 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 2216

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

This theorem is used by:  2sp  2225  19.2g  2227  nfim1  2238  axc16g  2299  drsb2  2305  axc11r  2403  axc15  2457  equvel  2491  sb4a  2515  dfsb1  2516  dfsb2  2528  drsb1  2530  nfsb4t  2534  sbco2  2546  sbco3  2548  sb9  2554  sbal1  2563  sbal2  2564  eujustALT  2603  2eu6  2687  ralcom2  3369  ceqsalgALT  3494  reu6  3692  rexdifi  4107  dfnfc2  4899  nfnid  5351  eusvnfb  5369  mosubopt  5498  dfid3  5564  fv3  6906  fvmptt  7017  fnoprabg  7546  fprlem1  8306  pssnn  9163  frrlem15  9739  kmlem16  10168  nd3  10592  axunndlem1  10598  axunnd  10599  axpowndlem1  10600  axregndlem1  10605  axregndlem2  10606  axacndlem5  10614  axsepg3  35578  axsepg3ALT  35579  axsepg5  35581  axnulg  35582  fundmpss  36280  nalfal  36955  unisym1  36975  axtcond  37030  bj-sbsb  37513  wl-nfimf1  38222  wl-axc11r  38226  wl-dral1d  38227  wl-nfs1t  38233  wl-sb8t  38248  wl-sbhbt  38250  wl-equsb4  38253  wl-sbalnae  38258  wl-2spsbbi  38261  wl-mo3t  38272  cotrintab  44381  pm11.57  45140  axc5c4c711toc7  45155  axc11next  45157  pm14.122b  45174  dropab1  45197  dropab2  45198  ax6e2eq  45307  quantgodelALT  47630