Theorem letr 11315

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11307	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1148	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 486	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 11311	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 11309	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1149	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 48	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 458	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 5115	. . . . . 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 2146   class class class wbr 5111  ℝcr 11110   < clt 11254   ≤ cle 11255

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-pre-lttri 11185  ax-pre-lttrn 11186

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260

This theorem is used by:  letri  11350  letrd  11378  le2add  11707  le2sub  11724  p1le  12071  lemul12b  12083  lemul12a  12084  zletr  12649  peano2uz2  12695  ledivge1le  13100  lemaxle  13232  elfz1b  13633  elfz0fzfz0  13673  fz0fzelfz0  13674  fz0fzdiffz0  13677  elfzmlbp  13679  difelfznle  13682  elincfzoext  13764  ssfzoulel  13801  ssfzo12bi  13802  flge  13851  flflp1  13853  fldiv4p1lem1div2  13881  fldiv4lem1div2uz2  13882  monoord  14081  le2sq2  14184  leexp2r  14223  expubnd  14227  facwordi  14338  faclbnd3  14341  facavg  14350  fi1uzind  14557  swrdswrdlem  14758  swrdccat  14789  01sqrexlem1  15312  01sqrexlem6  15317  01sqrexlem7  15318  leabs  15369  limsupbnd2  15553  rlim3  15568  lo1bdd2  15594  lo1bddrp  15595  o1lo1  15607  lo1mul  15698  lo1le  15722  isercolllem2  15736  iseraltlem2  15753  fsumabs  15871  cvgrat  15955  ruclem9  16311  algcvga  16654  prmdvdsfz  16781  prmfac1  16796  eulerthlem2  16858  modprm0  16882  prmreclem1  16993  prmreclem4  16996  4sqlem11  17032  vdwnnlem3  17074  zntoslem  21735  gsumbagdiaglem  22110  psdmul  22358  cnllycmp  25144  evth  25147  ovoliunlem2  25691  ovolicc2lem3  25707  itg2monolem1  25938  bddiblnc  26030  coeaddlem  26435  coemullem  26436  aalioulem5  26528  aalioulem6  26529  sincosq1lem  26691  emcllem6  27194  ftalem3  27268  fsumvma2  27407  chpchtsum  27412  bcmono  27470  bposlem5  27481  gausslemma2dlem1a  27558  lgsquadlem1  27573  dchrisum0lem1  27709  pntrsumbnd2  27760  pntleml  27804  brbtwn2  29284  axlowdimlem17  29337  axlowdim  29340  crctcshwlkn0lem3  30190  crctcshwlkn0lem5  30192  wwlksubclwwlk  30438  eupth2lems  30618  nmoub3i  31154  ubthlem1  31251  ubthlem2  31252  nmopub2tALT  32290  nmfnleub2  32307  lnconi  32414  leoptr  32518  pjnmopi  32529  cdj3lem2b  32818  eulerpartlemb  34782  isbasisrelowllem1  38034  isbasisrelowllem2  38035  ltflcei  38292  itg2addnclem2  38356  itg2addnclem3  38357  itg2addnc  38358  dvasin  38388  incsequz  38432  mettrifi  38441  equivbnd  38474  bfplem1  38506  jm2.17b  43721  fmul01lt1lem2  46334  eluzge0nn0  48082  elfz2z  48085  iccpartiltu  48204  iccpartgt  48209  lighneallem2  48391