Theorem letr 11308

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

Assertion

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

Proof of Theorem letr

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5109  ℝcr 11103   < clt 11247   ≤ cle 11248

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-pre-lttri 11178  ax-pre-lttrn 11179

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253

This theorem is used by:  letri  11343  letrd  11371  le2add  11700  le2sub  11717  p1le  12064  lemul12b  12076  lemul12a  12077  zletr  12642  peano2uz2  12688  ledivge1le  13093  lemaxle  13225  elfz1b  13626  elfz0fzfz0  13666  fz0fzelfz0  13667  fz0fzdiffz0  13670  elfzmlbp  13672  difelfznle  13675  elincfzoext  13757  ssfzoulel  13794  ssfzo12bi  13795  flge  13843  flflp1  13845  fldiv4p1lem1div2  13873  fldiv4lem1div2uz2  13874  monoord  14073  le2sq2  14176  leexp2r  14215  expubnd  14219  facwordi  14330  faclbnd3  14333  facavg  14342  fi1uzind  14549  swrdswrdlem  14746  swrdccat  14777  01sqrexlem1  15298  01sqrexlem6  15303  01sqrexlem7  15304  leabs  15355  limsupbnd2  15539  rlim3  15554  lo1bdd2  15580  lo1bddrp  15581  o1lo1  15593  lo1mul  15684  lo1le  15708  isercolllem2  15722  iseraltlem2  15739  fsumabs  15858  cvgrat  15942  ruclem9  16298  algcvga  16641  prmdvdsfz  16768  prmfac1  16783  eulerthlem2  16845  modprm0  16869  prmreclem1  16980  prmreclem4  16983  4sqlem11  17019  vdwnnlem3  17061  zntoslem  21715  gsumbagdiaglem  22090  psdmul  22338  cnllycmp  25124  evth  25127  ovoliunlem2  25671  ovolicc2lem3  25687  itg2monolem1  25918  bddiblnc  26010  coeaddlem  26415  coemullem  26416  aalioulem5  26508  aalioulem6  26509  sincosq1lem  26671  emcllem6  27174  ftalem3  27248  fsumvma2  27387  chpchtsum  27392  bcmono  27450  bposlem5  27461  gausslemma2dlem1a  27538  lgsquadlem1  27553  dchrisum0lem1  27689  pntrsumbnd2  27740  pntleml  27784  brbtwn2  29264  axlowdimlem17  29317  axlowdim  29320  crctcshwlkn0lem3  30170  crctcshwlkn0lem5  30172  wwlksubclwwlk  30418  eupth2lems  30598  nmoub3i  31134  ubthlem1  31231  ubthlem2  31232  nmopub2tALT  32270  nmfnleub2  32287  lnconi  32394  leoptr  32498  pjnmopi  32509  cdj3lem2b  32798  eulerpartlemb  34767  isbasisrelowllem1  38029  isbasisrelowllem2  38030  ltflcei  38287  itg2addnclem2  38351  itg2addnclem3  38352  itg2addnc  38353  dvasin  38383  incsequz  38427  mettrifi  38436  equivbnd  38469  bfplem1  38501  jm2.17b  43716  fmul01lt1lem2  46329  eluzge0nn0  48077  elfz2z  48080  iccpartiltu  48199  iccpartgt  48204  lighneallem2  48386