![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > rspcsbela | Unicode version |
Description: Special case related to rspsbc 3417. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3417 | . . 3 | |
2 | sbcel1g 3829 | . . 3 | |
3 | 1, 2 | sylibd 214 | . 2 |
4 | 3 | imp 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 |