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

Syntax hints:   → wi 4  ∀wal 1561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  2sp  2224  19.2g  2226  nfim1  2237  axc16g  2298  drsb2  2304  axc11r  2402  axc15  2456  equvel  2490  sb4a  2514  dfsb1  2515  dfsb2  2527  drsb1  2529  nfsb4t  2533  sbco2  2545  sbco3  2547  sb9  2553  sbal1  2562  sbal2  2563  eujustALT  2602  2eu6  2686  ralcom2  3367  ceqsalgALT  3493  reu6  3692  rexdifi  4106  dfnfc2  4890  nfnid  5337  eusvnfb  5355  mosubopt  5484  dfid3  5550  fv3  6889  fvmptt  7000  fnoprabg  7523  fprlem1  8285  pssnn  9141  frrlem15  9717  kmlem16  10137  nd3  10562  axunndlem1  10568  axunnd  10569  axpowndlem1  10570  axregndlem1  10575  axregndlem2  10576  axacndlem5  10584  axsepg3  35449  axsepg3ALT  35450  axsepg5  35452  axnulg  35453  fundmpss  36130  nalfal  36776  unisym1  36796  axtcond  36851  bj-sbsb  37334  wl-nfimf1  38041  wl-axc11r  38045  wl-dral1d  38046  wl-nfs1t  38052  wl-sb8t  38067  wl-sbhbt  38069  wl-equsb4  38072  wl-sbalnae  38077  wl-2spsbbi  38080  wl-mo3t  38091  cotrintab  44202  pm11.57  44963  axc5c4c711toc7  44978  axc11next  44980  pm14.122b  44997  dropab1  45020  dropab2  45021  ax6e2eq  45131  quantgodelALT  47447