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  2367  axc15  2421  equvel  2455  sb4a  2479  dfsb1  2480  dfsb2  2492  drsb1  2494  nfsb4t  2498  sbco2  2510  sbco3  2512  sb9  2518  sbal1  2527  sbal2  2528  eujustALT  2566  2eu6  2651  ralcom2  3353  ceqsalgALT  3487  reu6  3700  rexdifi  4116  dfnfc2  4896  nfnid  5333  eusvnfb  5351  mosubopt  5473  dfid3  5539  fv3  6879  fvmptt  6991  fnoprabg  7515  fprlem1  8282  pssnn  9138  frrlem15  9717  kmlem16  10126  nd3  10549  axunndlem1  10555  axunnd  10556  axpowndlem1  10557  axregndlem1  10562  axregndlem2  10563  axacndlem5  10571  axsepg2  35079  axsepg2ALT  35080  axnulg  35089  fundmpss  35761  nalfal  36398  unisym1  36418  bj-sbsb  36832  wl-nfimf1  37521  wl-axc11r  37525  wl-dral1d  37526  wl-nfs1t  37532  wl-sb8t  37547  wl-sbhbt  37549  wl-equsb4  37552  wl-sbalnae  37557  wl-2spsbbi  37560  wl-mo3t  37571  wl-ax11-lem5  37584  wl-ax11-lem8  37587  cotrintab  43610  pm11.57  44385  axc5c4c711toc7  44400  axc11next  44402  pm14.122b  44419  dropab1  44443  dropab2  44444  ax6e2eq  44554