Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcsbela Unicode version

Theorem rspcsbela 3853
 Description: Special case related to rspsbc 3417. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
Assertion
Ref Expression
rspcsbela
Distinct variable groups:   ,   ,

Proof of Theorem rspcsbela
StepHypRef Expression
1 rspsbc 3417 . . 3
2 sbcel1g 3829 . . 3
31, 2sylibd 214 . 2
43imp 429 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  A.wral 2807  [.wsbc 3327  [_csb 3434 This theorem is referenced by:  mptnn0fsupp  12103  mptnn0fsuppr  12105  fsumzcl2  13560  fsummsnunz  13569  fsumsplitsnun  13570  modfsummodslem1  13606  gsummpt1n0  16992  gsummptnn0fz  17014  telgsumfzslem  17017  telgsumfzs  17018  telgsums  17022  mptscmfsupp0  17576  coe1fzgsumdlem  18343  gsummoncoe1  18346  evl1gsumdlem  18392  madugsum  19145  iunmbl2  21967  gsumvsca1  27773  gsumvsca2  27774  iblsplitf  31769  fsummsndifre  32345  fsumsplitsndif  32346  fsummmodsndifre  32347  fsummmodsnunz  32348 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785
 Copyright terms: Public domain W3C validator