Theorem letr 10169

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 10162	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1099	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 480	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 10166	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 10164	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1100	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 47	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 452	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 4689	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 239	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 481	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 394	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 230	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 628	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   class class class wbr 4685  ℝcr 9973   < clt 10112   ≤ cle 10113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttri 10048  ax-pre-lttrn 10049

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118

This theorem is referenced by:  letri  10204  letrd  10232  le2add  10548  le2sub  10565  p1le  10904  lemul12b  10918  lemul12a  10919  zletr  11459  peano2uz2  11503  ledivge1le  11939  lemaxle  12064  elfz1b  12447  elfz0fzfz0  12483  fz0fzelfz0  12484  fz0fzdiffz0  12487  elfzmlbp  12489  difelfznle  12492  elincfzoext  12565  ssfzoulel  12602  ssfzo12bi  12603  flge  12646  flflp1  12648  fldiv4p1lem1div2  12676  fldiv4lem1div2uz2  12677  monoord  12871  leexp2r  12958  expubnd  12961  le2sq2  12979  facwordi  13116  faclbnd3  13119  facavg  13128  fi1uzind  13317  swrdswrdlem  13505  swrdccat  13539  sqrlem1  14027  sqrlem6  14032  sqrlem7  14033  leabs  14083  limsupbnd2  14258  rlim3  14273  lo1bdd2  14299  lo1bddrp  14300  o1lo1  14312  lo1mul  14402  lo1le  14426  isercolllem2  14440  iseraltlem2  14457  fsumabs  14577  cvgrat  14659  ruclem9  15011  algcvga  15339  prmdvdsfz  15464  prmfac1  15478  eulerthlem2  15534  modprm0  15557  prmreclem1  15667  prmreclem4  15670  4sqlem11  15706  vdwnnlem3  15748  gsumbagdiaglem  19423  zntoslem  19953  cnllycmp  22802  evth  22805  ovoliunlem2  23317  ovolicc2lem3  23333  itg2monolem1  23562  coeaddlem  24050  coemullem  24051  aalioulem5  24136  aalioulem6  24137  sincosq1lem  24294  emcllem6  24772  ftalem3  24846  fsumvma2  24984  chpchtsum  24989  bcmono  25047  bposlem5  25058  gausslemma2dlem1a  25135  lgsquadlem1  25150  dchrisum0lem1  25250  pntrsumbnd2  25301  pntleml  25345  brbtwn2  25830  axlowdimlem17  25883  axlowdim  25886  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  wwlksubclwwlk  27023  clwlksfclwwlk  27049  eupth2lems  27216  nmoub3i  27756  ubthlem1  27854  ubthlem2  27855  nmopub2tALT  28896  nmfnleub2  28913  lnconi  29020  leoptr  29124  pjnmopi  29135  cdj3lem2b  29424  eulerpartlemb  30558  isbasisrelowllem1  33333  isbasisrelowllem2  33334  ltflcei  33527  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  bddiblnc  33610  dvasin  33626  incsequz  33674  mettrifi  33683  equivbnd  33719  bfplem1  33751  jm2.17b  37845  fmul01lt1lem2  40135  eluzge0nn0  41647  elfz2z  41650  iccpartiltu  41683  iccpartgt  41688  lighneallem2  41848