Theorem letr 10010

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 10003	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1072	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 480	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 10007	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 10005	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1073	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 46	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 452	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 4587	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 238	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 481	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 394	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 229	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 627	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  letri  10045  letrd  10073  le2add  10389  le2sub  10406  p1le  10745  lemul12b  10759  lemul12a  10760  zletr  11298  peano2uz2  11341  ledivge1le  11777  lemaxle  11900  elfz1b  12279  elfz0fzfz0  12313  fz0fzelfz0  12314  fz0fzdiffz0  12317  elfzmlbp  12319  difelfznle  12322  elincfzoext  12393  ssfzoulel  12428  ssfzo12bi  12429  flge  12468  flflp1  12470  fldiv4p1lem1div2  12498  fldiv4lem1div2uz2  12499  monoord  12693  leexp2r  12780  expubnd  12783  le2sq2  12801  facwordi  12938  faclbnd3  12941  facavg  12950  fi1uzind  13134  fi1uzindOLD  13140  swrdswrdlem  13311  swrdccat  13344  sqrlem1  13831  sqrlem6  13836  sqrlem7  13837  leabs  13887  limsupbnd2  14062  rlim3  14077  lo1bdd2  14103  lo1bddrp  14104  o1lo1  14116  lo1mul  14206  lo1le  14230  isercolllem2  14244  iseraltlem2  14261  fsumabs  14374  cvgrat  14454  ruclem9  14806  algcvga  15130  prmdvdsfz  15255  prmfac1  15269  eulerthlem2  15325  modprm0  15348  prmreclem1  15458  prmreclem4  15461  4sqlem11  15497  vdwnnlem3  15539  gsumbagdiaglem  19196  zntoslem  19724  cnllycmp  22563  evth  22566  ovoliunlem2  23078  ovolicc2lem3  23094  itg2monolem1  23323  coeaddlem  23809  coemullem  23810  aalioulem5  23895  aalioulem6  23896  sincosq1lem  24053  emcllem6  24527  ftalem3  24601  fsumvma2  24739  chpchtsum  24744  bcmono  24802  bposlem5  24813  gausslemma2dlem1a  24890  lgsquadlem1  24905  dchrisum0lem1  25005  pntrsumbnd2  25056  pntleml  25100  brbtwn2  25585  axlowdimlem17  25638  axlowdim  25641  wwlksubclwwlk  26332  clwlkfclwwlk  26371  eupath2  26507  nmoub3i  27012  ubthlem1  27110  ubthlem2  27111  nmopub2tALT  28152  nmfnleub2  28169  lnconi  28276  leoptr  28380  pjnmopi  28391  cdj3lem2b  28680  eulerpartlemb  29757  isbasisrelowllem1  32379  isbasisrelowllem2  32380  ltflcei  32567  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  bddiblnc  32650  dvasin  32666  incsequz  32714  mettrifi  32723  equivbnd  32759  bfplem1  32791  jm2.17b  36546  fmul01lt1lem2  38652  iccpartiltu  39960  iccpartgt  39965  lighneallem2  40061  eluzge0nn0  40350  elfz2z  40352  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  wwlksubclwwlks  41232  clwlksfclwwlk  41269  eupth2lems  41406