Theorem sps 2179

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 2177	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 17	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2sp  2180  19.2g  2182  nfim1  2193  axc16g  2252  drsb2  2258  axc11r  2366  axc15  2422  equvel  2456  sb4a  2480  dfsb1  2481  dfsb2  2493  drsb1  2495  nfsb4t  2499  sbco2  2511  sbco3  2513  sb9  2519  sbal1  2528  sbal2  2529  eujustALT  2567  2eu6  2653  ralcom2  3374  ceqsalgALT  3509  reu6  3723  sbcal  3842  rexdifi  4146  reldisjOLD  4453  dfnfc2  4934  nfnid  5374  eusvnfb  5392  mosubopt  5511  dfid3  5578  fv3  6910  fvmptt  7019  fnoprabg  7531  fprlem1  8285  wfrlem5OLD  8313  pssnn  9168  pssnnOLD  9265  frrlem15  9752  kmlem16  10160  nd3  10584  axunndlem1  10590  axunnd  10591  axpowndlem1  10592  axregndlem1  10597  axregndlem2  10598  axacndlem5  10606  fundmpss  34738  nalfal  35288  unisym1  35308  bj-sbsb  35715  wl-nfimf1  36395  wl-axc11r  36399  wl-dral1d  36400  wl-nfs1t  36406  wl-sb8t  36417  wl-sbhbt  36419  wl-equsb4  36422  wl-sbalnae  36427  wl-2spsbbi  36430  wl-mo3t  36441  wl-ax11-lem5  36451  wl-ax11-lem8  36454  cotrintab  42365  pm11.57  43148  axc5c4c711toc7  43163  axc11next  43165  pm14.122b  43182  dropab1  43206  dropab2  43207  ax6e2eq  43318