MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sps Structured version   Visualization version   GIF version

Theorem sps 2219
Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
Hypothesis
Ref Expression
sps.1 (𝜑𝜓)
Assertion
Ref Expression
sps (∀𝑥𝜑𝜓)

Proof of Theorem sps
StepHypRef Expression
1 sp 2217 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 17 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-12 2213
This theorem depends on definitions:  df-bi 199  df-ex 1876
This theorem is referenced by:  2sp  2220  19.2g  2222  nfim1  2231  axc16g  2282  axc11r  2376  axc15  2429  equvel  2463  dfsb2  2490  drsb1  2494  drsb2  2495  nfsb4t  2506  sbi1  2509  sbco2  2533  sbco3  2535  sb9  2544  sbal1  2579  eujustALT  2612  2eu6  2714  ralcom2  3285  ceqsalgALT  3419  reu6  3591  sbcal  3683  reldisj  4215  dfnfc2  4648  nfnid  5045  eusvnfb  5063  mosubopt  5166  dfid3  5221  idrefOLD  5727  fv3  6429  fvmptt  6525  fnoprabg  6995  wfrlem5  7658  pssnn  8420  kmlem16  9275  nd3  9699  axunndlem1  9705  axunnd  9706  axpowndlem1  9707  axregndlem1  9712  axregndlem2  9713  axacndlem5  9721  fundmpss  32178  frrlem5  32297  nalfal  32910  unisym1  32930  bj-sbsb  33319  bj-mo3OLD  33327  bj-ax9  33381  wl-nfimf1  33803  wl-dral1d  33808  wl-nfs1t  33814  wl-sb8t  33824  wl-sbhbt  33826  wl-equsb4  33829  wl-sbalnae  33835  wl-mo3t  33848  wl-ax11-lem5  33856  wl-ax11-lem8  33859  cotrintab  38704  pm11.57  39371  axc5c4c711toc7  39386  axc11next  39388  pm14.122b  39405  dropab1  39431  dropab2  39432  ax6e2eq  39543
  Copyright terms: Public domain W3C validator