Theorem letr 11231

Description: Transitive law. (Contributed by NM, 12-Nov-1999.)

Assertion

Ref	Expression
letr	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11223	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1136	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 481	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 11227	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 11225	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1137	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 47	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 453	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 5076	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 250	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 482	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 865	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 241	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 454	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  letri  11266  letrd  11294  le2add  11623  le2sub  11640  p1le  11991  lemul12b  12003  lemul12a  12004  zletr  12562  peano2uz2  12608  ledivge1le  13006  lemaxle  13138  elfz1b  13538  elfz0fzfz0  13578  fz0fzelfz0  13579  fz0fzdiffz0  13582  elfzmlbp  13584  difelfznle  13587  elincfzoext  13669  ssfzoulel  13706  ssfzo12bi  13707  flge  13755  flflp1  13757  fldiv4p1lem1div2  13785  fldiv4lem1div2uz2  13786  monoord  13985  le2sq2  14088  leexp2r  14127  expubnd  14131  facwordi  14242  faclbnd3  14245  facavg  14254  fi1uzind  14460  swrdswrdlem  14657  swrdccat  14688  01sqrexlem1  15195  01sqrexlem6  15200  01sqrexlem7  15201  leabs  15252  limsupbnd2  15436  rlim3  15451  lo1bdd2  15477  lo1bddrp  15478  o1lo1  15490  lo1mul  15581  lo1le  15605  isercolllem2  15619  iseraltlem2  15636  fsumabs  15755  cvgrat  15839  ruclem9  16196  algcvga  16539  prmdvdsfz  16666  prmfac1  16681  eulerthlem2  16743  modprm0  16767  prmreclem1  16878  prmreclem4  16881  4sqlem11  16917  vdwnnlem3  16959  zntoslem  21531  gsumbagdiaglem  21906  psdmul  22154  cnllycmp  24941  evth  24944  ovoliunlem2  25488  ovolicc2lem3  25504  itg2monolem1  25735  bddiblnc  25827  coeaddlem  26232  coemullem  26233  aalioulem5  26320  aalioulem6  26321  sincosq1lem  26479  emcllem6  26982  ftalem3  27056  fsumvma2  27195  chpchtsum  27200  bcmono  27258  bposlem5  27269  gausslemma2dlem1a  27346  lgsquadlem1  27361  dchrisum0lem1  27497  pntrsumbnd2  27548  pntleml  27592  brbtwn2  28992  axlowdimlem17  29045  axlowdim  29048  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  wwlksubclwwlk  30146  eupth2lems  30326  nmoub3i  30862  ubthlem1  30959  ubthlem2  30960  nmopub2tALT  31998  nmfnleub2  32015  lnconi  32122  leoptr  32226  pjnmopi  32237  cdj3lem2b  32526  eulerpartlemb  34552  isbasisrelowllem1  37717  isbasisrelowllem2  37718  ltflcei  37975  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  dvasin  38071  incsequz  38115  mettrifi  38124  equivbnd  38157  bfplem1  38189  jm2.17b  43406  fmul01lt1lem2  46030  eluzge0nn0  47775  elfz2z  47778  iccpartiltu  47897  iccpartgt  47902  lighneallem2  48084