![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspcsbela | Structured version Visualization version Unicode version |
Description: Special case related to rspsbc 3348. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3348 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sbcel1g 3778 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylibd 218 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | imp 431 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1449 df-fal 1452 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ral 2744 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-in 3413 df-ss 3420 df-nul 3734 |
This theorem is referenced by: mptnn0fsupp 12216 mptnn0fsuppr 12218 fsumzcl2 13816 fsummsnunz 13827 fsumsplitsnun 13828 modfsummodslem1 13864 gsummpt1n0 17609 gsummptnn0fz 17627 telgsumfzslem 17630 telgsumfzs 17631 telgsums 17635 mptscmfsupp0 18165 coe1fzgsumdlem 18907 gsummoncoe1 18910 evl1gsumdlem 18956 madugsum 19680 iunmbl2 22522 gsumvsca1 28557 gsumvsca2 28558 esum2dlem 28925 esumiun 28927 iblsplitf 37857 fsummsndifre 39101 fsumsplitsndif 39102 fsummmodsndifre 39103 fsummmodsnunz 39104 |
Copyright terms: Public domain | W3C validator |