![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lecasei | Structured version Visualization version Unicode version |
Description: Ordering elimination by cases. (Contributed by NM, 6-Jul-2007.) |
Ref | Expression |
---|---|
lecase.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lecase.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lecase.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lecase.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lecasei |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lecase.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | lecase.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | lecase.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | lecase.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | letric 9765 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | syl2anc 671 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 6 | mpjaodan 800 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-resscn 9627 ax-pre-lttri 9644 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-br 4419 df-opab 4478 df-mpt 4479 df-id 4771 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-er 7394 df-en 7601 df-dom 7602 df-sdom 7603 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 |
This theorem is referenced by: wloglei 10179 nn2ge 10667 max0sub 11523 leabs 13417 max0add 13428 limsupgre 13597 limsupgreOLD 13598 ntrivcvgmul 14013 1arithlem4 14925 mndodcong 17246 metustto 21623 reconn 21901 dyaddisj 22610 volcn 22620 ditgcl 22869 ditgswap 22870 ditgsplit 22872 dvfsumlem3 23036 ftc2ditg 23054 coseq0negpitopi 23514 asinlem3 23853 atanlogaddlem 23895 atanlogadd 23896 ppiub 24188 dchrisum0 24414 pntrmax 24458 padicabv 24524 nacsfix 35600 acongrep 35876 hbt 36035 |
Copyright terms: Public domain | W3C validator |