Theorem sps 2186

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2sp  2187  19.2g  2189  nfim1  2200  axc16g  2261  drsb2  2267  axc11r  2366  axc15  2420  equvel  2454  sb4a  2478  dfsb1  2479  dfsb2  2491  drsb1  2493  nfsb4t  2497  sbco2  2509  sbco3  2511  sb9  2517  sbal1  2526  sbal2  2527  eujustALT  2565  2eu6  2650  ralcom2  3351  ceqsalgALT  3484  reu6  3697  rexdifi  4113  dfnfc2  4893  nfnid  5330  eusvnfb  5348  mosubopt  5470  dfid3  5536  fv3  6876  fvmptt  6988  fnoprabg  7512  fprlem1  8279  pssnn  9132  frrlem15  9710  kmlem16  10119  nd3  10542  axunndlem1  10548  axunnd  10549  axpowndlem1  10550  axregndlem1  10555  axregndlem2  10556  axacndlem5  10564  axsepg2  35072  axsepg2ALT  35073  axnulg  35082  fundmpss  35754  nalfal  36391  unisym1  36411  bj-sbsb  36825  wl-nfimf1  37514  wl-axc11r  37518  wl-dral1d  37519  wl-nfs1t  37525  wl-sb8t  37540  wl-sbhbt  37542  wl-equsb4  37545  wl-sbalnae  37550  wl-2spsbbi  37553  wl-mo3t  37564  wl-ax11-lem5  37577  wl-ax11-lem8  37580  cotrintab  43603  pm11.57  44378  axc5c4c711toc7  44393  axc11next  44395  pm14.122b  44412  dropab1  44436  dropab2  44437  ax6e2eq  44547