![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > letr | Structured version Visualization version GIF version |
Description: Transitive law. (Contributed by NM, 12-Nov-1999.) |
Ref | Expression |
---|---|
letr | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leloe 11296 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) | |
2 | 1 | 3adant1 1130 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
3 | 2 | adantr 481 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶))) |
4 | lelttr 11300 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) | |
5 | ltle 11298 | . . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) | |
6 | 5 | 3adant2 1131 | . . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶)) |
7 | 4, 6 | syld 47 | . . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶)) |
8 | 7 | expdimp 453 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶)) |
9 | breq2 5151 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶)) | |
10 | 9 | biimpcd 248 | . . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
11 | 10 | adantl 482 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶)) |
12 | 8, 11 | jaod 857 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶)) |
13 | 3, 12 | sylbid 239 | . 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶)) |
14 | 13 | expimpd 454 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 class class class wbr 5147 ℝcr 11105 < clt 11244 ≤ cle 11245 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-resscn 11163 ax-pre-lttri 11180 ax-pre-lttrn 11181 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 |
This theorem is referenced by: letri 11339 letrd 11367 le2add 11692 le2sub 11709 p1le 12055 lemul12b 12067 lemul12a 12068 zletr 12602 peano2uz2 12646 ledivge1le 13041 lemaxle 13170 elfz1b 13566 elfz0fzfz0 13602 fz0fzelfz0 13603 fz0fzdiffz0 13606 elfzmlbp 13608 difelfznle 13611 elincfzoext 13686 ssfzoulel 13722 ssfzo12bi 13723 flge 13766 flflp1 13768 fldiv4p1lem1div2 13796 fldiv4lem1div2uz2 13797 monoord 13994 le2sq2 14096 leexp2r 14135 expubnd 14138 facwordi 14245 faclbnd3 14248 facavg 14257 fi1uzind 14454 swrdswrdlem 14650 swrdccat 14681 01sqrexlem1 15185 01sqrexlem6 15190 01sqrexlem7 15191 leabs 15242 limsupbnd2 15423 rlim3 15438 lo1bdd2 15464 lo1bddrp 15465 o1lo1 15477 lo1mul 15568 lo1le 15594 isercolllem2 15608 iseraltlem2 15625 fsumabs 15743 cvgrat 15825 ruclem9 16177 algcvga 16512 prmdvdsfz 16638 prmfac1 16654 eulerthlem2 16711 modprm0 16734 prmreclem1 16845 prmreclem4 16848 4sqlem11 16884 vdwnnlem3 16926 zntoslem 21103 gsumbagdiaglemOLD 21482 gsumbagdiaglem 21485 cnllycmp 24463 evth 24466 ovoliunlem2 25011 ovolicc2lem3 25027 itg2monolem1 25259 bddiblnc 25350 coeaddlem 25754 coemullem 25755 aalioulem5 25840 aalioulem6 25841 sincosq1lem 25998 emcllem6 26494 ftalem3 26568 fsumvma2 26706 chpchtsum 26711 bcmono 26769 bposlem5 26780 gausslemma2dlem1a 26857 lgsquadlem1 26872 dchrisum0lem1 27008 pntrsumbnd2 27059 pntleml 27103 brbtwn2 28152 axlowdimlem17 28205 axlowdim 28208 crctcshwlkn0lem3 29055 crctcshwlkn0lem5 29057 wwlksubclwwlk 29300 eupth2lems 29480 nmoub3i 30013 ubthlem1 30110 ubthlem2 30111 nmopub2tALT 31149 nmfnleub2 31166 lnconi 31273 leoptr 31377 pjnmopi 31388 cdj3lem2b 31677 eulerpartlemb 33355 isbasisrelowllem1 36224 isbasisrelowllem2 36225 ltflcei 36464 itg2addnclem2 36528 itg2addnclem3 36529 itg2addnc 36530 dvasin 36560 incsequz 36604 mettrifi 36613 equivbnd 36646 bfplem1 36678 jm2.17b 41685 fmul01lt1lem2 44287 eluzge0nn0 46006 elfz2z 46009 iccpartiltu 46076 iccpartgt 46081 lighneallem2 46260 |
Copyright terms: Public domain | W3C validator |