Theorem letr 10570

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

Assertion

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

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 10563	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1121	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3	2	adantr 481	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
4		lelttr 10567	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
5		ltle 10565	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
6	5	3adant2 1122	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶 → 𝐴 ≤ 𝐶))
7	4, 6	syld 47	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 ≤ 𝐶))
8	7	expdimp 453	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 < 𝐶 → 𝐴 ≤ 𝐶))
9		breq2 4960	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ 𝐶))
10	9	biimpcd 250	. . . . 5 ⊢ (𝐴 ≤ 𝐵 → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
11	10	adantl 482	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 = 𝐶 → 𝐴 ≤ 𝐶))
12	8, 11	jaod 854	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → 𝐴 ≤ 𝐶))
13	3, 12	sylbid 241	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐵 ≤ 𝐶 → 𝐴 ≤ 𝐶))
14	13	expimpd 454	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   ∧ w3a 1078   = wceq 1520   ∈ wcel 2079   class class class wbr 4956  ℝcr 10371   < clt 10510   ≤ cle 10511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-resscn 10429  ax-pre-lttri 10446  ax-pre-lttrn 10447

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516

This theorem is referenced by:  letri  10605  letrd  10633  le2add  10959  le2sub  10976  p1le  11322  lemul12b  11334  lemul12a  11335  zletr  11864  peano2uz2  11908  ledivge1le  12299  lemaxle  12427  elfz1b  12815  elfz0fzfz0  12851  fz0fzelfz0  12852  fz0fzdiffz0  12855  elfzmlbp  12857  difelfznle  12860  elincfzoext  12933  ssfzoulel  12969  ssfzo12bi  12970  flge  13013  flflp1  13015  fldiv4p1lem1div2  13043  fldiv4lem1div2uz2  13044  monoord  13238  le2sq2  13338  leexp2r  13376  expubnd  13379  facwordi  13487  faclbnd3  13490  facavg  13499  fi1uzind  13689  swrdswrdlem  13890  swrdccat  13921  sqrlem1  14424  sqrlem6  14429  sqrlem7  14430  leabs  14481  limsupbnd2  14662  rlim3  14677  lo1bdd2  14703  lo1bddrp  14704  o1lo1  14716  lo1mul  14806  lo1le  14830  isercolllem2  14844  iseraltlem2  14861  fsumabs  14977  cvgrat  15060  ruclem9  15412  algcvga  15740  prmdvdsfz  15866  prmfac1  15880  eulerthlem2  15936  modprm0  15959  prmreclem1  16069  prmreclem4  16072  4sqlem11  16108  vdwnnlem3  16150  gsumbagdiaglem  19831  zntoslem  20373  cnllycmp  23231  evth  23234  ovoliunlem2  23775  ovolicc2lem3  23791  itg2monolem1  24022  coeaddlem  24510  coemullem  24511  aalioulem5  24596  aalioulem6  24597  sincosq1lem  24754  emcllem6  25248  ftalem3  25322  fsumvma2  25460  chpchtsum  25465  bcmono  25523  bposlem5  25534  gausslemma2dlem1a  25611  lgsquadlem1  25626  dchrisum0lem1  25762  pntrsumbnd2  25813  pntleml  25857  brbtwn2  26362  axlowdimlem17  26415  axlowdim  26418  crctcshwlkn0lem3  27265  crctcshwlkn0lem5  27267  wwlksubclwwlk  27512  eupth2lems  27693  nmoub3i  28229  ubthlem1  28326  ubthlem2  28327  nmopub2tALT  29365  nmfnleub2  29382  lnconi  29489  leoptr  29593  pjnmopi  29604  cdj3lem2b  29893  eulerpartlemb  31199  isbasisrelowllem1  34113  isbasisrelowllem2  34114  ltflcei  34357  itg2addnclem2  34421  itg2addnclem3  34422  itg2addnc  34423  bddiblnc  34439  dvasin  34455  incsequz  34501  mettrifi  34510  equivbnd  34546  bfplem1  34578  jm2.17b  38994  fmul01lt1lem2  41362  eluzge0nn0  42982  elfz2z  42985  iccpartiltu  43018  iccpartgt  43023  lighneallem2  43207