Theorem letr 11328

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11320	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1148	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 486	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 11324	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 11322	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1149	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 48	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 458	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 5107	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 252	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 487	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 873	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 243	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 459	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ℝcr 11123   < clt 11267   ≤ cle 11268

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198  ax-pre-lttrn 11199

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  letri  11363  letrd  11391  le2add  11720  le2sub  11737  p1le  12084  lemul12b  12096  lemul12a  12097  zletr  12662  peano2uz2  12709  ledivge1le  13115  lemaxle  13247  elfz1b  13648  elfz0fzfz0  13688  fz0fzelfz0  13689  fz0fzdiffz0  13692  elfzmlbp  13694  difelfznle  13697  elincfzoext  13779  ssfzoulel  13816  ssfzo12bi  13817  flge  13866  flflp1  13868  fldiv4p1lem1div2  13896  fldiv4lem1div2uz2  13897  monoord  14096  le2sq2  14199  leexp2r  14238  expubnd  14242  facwordi  14353  faclbnd3  14356  facavg  14365  fi1uzind  14572  swrdswrdlem  14773  swrdccat  14804  01sqrexlem1  15329  01sqrexlem6  15334  01sqrexlem7  15335  leabs  15386  limsupbnd2  15570  rlim3  15585  lo1bdd2  15611  lo1bddrp  15612  o1lo1  15624  lo1mul  15715  lo1le  15739  isercolllem2  15753  iseraltlem2  15770  fsumabs  15888  cvgrat  15972  ruclem9  16326  algcvga  16669  prmdvdsfz  16796  prmfac1  16811  eulerthlem2  16873  modprm0  16897  prmreclem1  17008  prmreclem4  17011  4sqlem11  17047  vdwnnlem3  17089  zntoslem  21769  gsumbagdiaglem  22146  psdmul  22394  cnllycmp  25184  evth  25187  ovoliunlem2  25731  ovolicc2lem3  25747  itg2monolem1  25978  bddiblnc  26069  coeaddlem  26475  coemullem  26476  aalioulem5  26572  aalioulem6  26573  sincosq1lem  26735  emcllem6  27237  ftalem3  27311  fsumvma2  27450  chpchtsum  27455  bcmono  27513  bposlem5  27524  gausslemma2dlem1a  27601  lgsquadlem1  27616  dchrisum0lem1  27752  pntrsumbnd2  27803  pntleml  27847  brbtwn2  29362  axlowdimlem17  29415  axlowdim  29418  crctcshwlkn0lem3  30280  crctcshwlkn0lem5  30282  wwlksubclwwlk  30528  eupth2lems  30718  nmoub3i  31254  ubthlem1  31351  ubthlem2  31352  nmopub2tALT  32390  nmfnleub2  32407  lnconi  32514  leoptr  32618  pjnmopi  32629  cdj3lem2b  32918  eulerpartlemb  34879  isbasisrelowllem1  38109  isbasisrelowllem2  38110  ltflcei  38362  itg2addnclem2  38421  itg2addnclem3  38422  itg2addnc  38423  dvasin  38453  incsequz  38498  mettrifi  38507  equivbnd  38540  bfplem1  38572  jm2.17b  43802  fmul01lt1lem2  46415  eluzge0nn0  48200  elfz2z  48203  iccpartiltu  48322  iccpartgt  48327  lighneallem2  48509