Theorem sps 2188

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

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

This theorem is referenced by:  2sp  2189  19.2g  2191  nfim1  2202  axc16g  2263  drsb2  2269  axc11r  2368  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  2652  ralcom2  3343  ceqsalgALT  3473  reu6  3685  rexdifi  4100  dfnfc2  4881  nfnid  5313  eusvnfb  5331  mosubopt  5450  dfid3  5514  fv3  6840  fvmptt  6949  fnoprabg  7469  fprlem1  8230  pssnn  9078  frrlem15  9647  kmlem16  10054  nd3  10477  axunndlem1  10483  axunnd  10484  axpowndlem1  10485  axregndlem1  10490  axregndlem2  10491  axacndlem5  10499  axsepg2  35089  axsepg2ALT  35090  axnulg  35110  fundmpss  35799  nalfal  36436  unisym1  36456  bj-sbsb  36870  wl-nfimf1  37559  wl-axc11r  37563  wl-dral1d  37564  wl-nfs1t  37570  wl-sb8t  37585  wl-sbhbt  37587  wl-equsb4  37590  wl-sbalnae  37595  wl-2spsbbi  37598  wl-mo3t  37609  wl-ax11-lem5  37622  wl-ax11-lem8  37625  cotrintab  43646  pm11.57  44421  axc5c4c711toc7  44436  axc11next  44438  pm14.122b  44455  dropab1  44478  dropab2  44479  ax6e2eq  44589