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

Step	Hyp	Ref	Expression
1		rspsbc 3417	. . 3
2		sbcel1g 3829	. . 3
3	1, 2	sylibd 214	. 2
4	3	imp 429	1

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