Theorem letr 11408

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 11400	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1148	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 486	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		leltletr 11405	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
5	4	expdimp 458	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
6		breq2 5106	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
7	6	biimpcd 252	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
8	7	adantl 487	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
9	5, 8	jaod 873	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
10	3, 9	sylbid 243	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
11	10	expimpd 459	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   class class class wbr 5102  ℝcr 11203   < clt 11347   ≤ cle 11348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-pre-lttri 11278  ax-pre-lttrn 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353

This theorem is used by:  letri  11443  letrd  11471  le2add  11802  le2sub  11819  p1le  12166  lemul12b  12178  lemul12a  12179  zletr  12744  peano2uz2  12791  ledivge1le  13197  lemaxle  13329  elfz1b  13731  elfz0fzfz0  13771  fz0fzelfz0  13772  fz0fzdiffz0  13775  elfzmlbp  13777  difelfznle  13780  elincfzoext  13862  ssfzoulel  13899  ssfzo12bi  13900  flge  13949  flflp1  13951  fldiv4p1lem1div2  13979  fldiv4lem1div2uz2  13980  monoord  14179  le2sq2  14282  leexp2r  14321  expubnd  14325  facwordi  14437  faclbnd3  14440  facavg  14449  fi1uzind  14656  swrdswrdlem  14858  swrdccat  14889  01sqrexlem1  15415  01sqrexlem6  15420  01sqrexlem7  15421  leabs  15472  limsupbnd2  15656  rlim3  15671  lo1bdd2  15697  lo1bddrp  15698  o1lo1  15710  lo1mul  15801  lo1le  15825  isercolllem2  15839  iseraltlem2  15856  fsumabs  15974  cvgrat  16058  ruclem9  16412  algcvga  16760  prmdvdsfz  16887  prmfac1  16902  eulerthlem2  16965  modprm0  16989  prmreclem1  17100  prmreclem4  17103  4sqlem11  17139  vdwnnlem3  17181  zntoslem  21868  gsumbagdiaglem  22245  psdmul  22493  cnllycmp  25283  evth  25286  ovoliunlem2  25830  ovolicc2lem3  25846  itg2monolem1  26077  bddiblnc  26168  coeaddlem  26574  coemullem  26575  aalioulem5  26669  aalioulem6  26670  sincosq1lem  26832  emcllem6  27334  ftalem3  27408  fsumvma2  27547  chpchtsum  27552  bcmono  27610  bposlem5  27621  gausslemma2dlem1a  27698  lgsquadlem1  27713  dchrisum0lem1  27849  pntrsumbnd2  27900  pntleml  27944  brbtwn2  29489  axlowdimlem17  29542  axlowdim  29545  crctcshwlkn0lem3  30407  crctcshwlkn0lem5  30409  wwlksubclwwlk  30655  eupth2lems  30845  nmoub3i  31381  ubthlem1  31478  ubthlem2  31479  nmopub2tALT  32517  nmfnleub2  32534  lnconi  32641  leoptr  32745  pjnmopi  32756  cdj3lem2b  33045  eulerpartlemb  35047  isbasisrelowllem1  38372  isbasisrelowllem2  38373  ltflcei  38625  itg2addnclem2  38684  itg2addnclem3  38685  itg2addnc  38686  dvasin  38716  incsequz  38776  mettrifi  38785  equivbnd  38818  bfplem1  38850  jm2.17b  44062  fmul01lt1lem2  46691  eluzge0nn0  48476  elfz2z  48479  iccpartiltu  48598  iccpartgt  48603  lighneallem2  48785