![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lelttr | Structured version Visualization version Unicode version |
Description: Transitive law. (Contributed by NM, 23-May-1999.) |
Ref | Expression |
---|---|
lelttr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leloe 9720 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3adant3 1028 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | lttr 9710 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | expd 438 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | breq1 4405 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | biimprd 227 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | a1i 11 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | jaod 382 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 2, 8 | sylbid 219 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | impd 433 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-resscn 9596 ax-pre-lttri 9613 ax-pre-lttrn 9614 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 |
This theorem is referenced by: letr 9727 lelttri 9761 lelttrd 9793 letrp1 10447 ltmul12a 10461 ledivp1 10508 supmul1 10576 bndndx 10868 uzind 11027 fnn0ind 11034 rpnnen1lem5 11294 xrinfmsslem 11593 elfzo0z 11958 fzofzim 11962 elfzodifsumelfzo 11980 flge 12041 flflp1 12043 flltdivnn0lt 12065 fsequb 12188 expnlbnd2 12403 ccat2s1fvw 12771 swrdswrd 12816 swrdccatin12lem3 12846 repswswrd 12887 caubnd2 13420 caubnd 13421 mulcn2 13659 cn1lem 13661 rlimo1 13680 o1rlimmul 13682 climsqz 13704 climsqz2 13705 rlimsqzlem 13712 climsup 13733 caucvgrlem2 13740 iseralt 13751 cvgcmp 13876 cvgcmpce 13878 ruclem3 14285 ruclem12 14293 algcvgblem 14536 ncoprmlnprm 14677 pclem 14788 infpn2 14857 gsummoncoe1 18898 mp2pm2mplem4 19833 metss2lem 21526 ngptgp 21644 nghmcn 21766 iocopnst 21968 ovollb2lem 22441 ovolicc2lem4OLD 22473 ovolicc2lem4 22474 volcn 22564 ismbf3d 22610 dvcnvrelem1 22969 dvfsumrlim 22983 ulmcn 23354 mtest 23359 logdivlti 23569 isosctrlem1 23747 ftalem2 23998 chtub 24140 bposlem6 24217 chtppilim 24313 dchrisumlem3 24329 pntlem3 24447 nvnencycllem 25371 clwlkisclwwlklem2a 25513 vacn 26330 nmcvcn 26331 blocni 26446 chscllem2 27291 lnconi 27686 staddi 27899 stadd3i 27901 ltflcei 31933 poimirlem29 31969 geomcau 32088 heibor1lem 32141 bfplem2 32155 rrncmslem 32164 climinf 37684 climinfOLD 37685 leltletr 38714 iccpartigtl 38737 tgoldbach 38911 zm1nn 39049 ply1mulgsumlem2 40232 difmodm1lt 40378 |
Copyright terms: Public domain | W3C validator |