MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  letr Structured version   Visualization version   GIF version

Theorem letr 10723
Description: Transitive law. (Contributed by NM, 12-Nov-1999.)
Assertion
Ref Expression
letr ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Proof of Theorem letr
StepHypRef Expression
1 leloe 10716 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
213adant1 1122 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
32adantr 481 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
4 lelttr 10720 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
5 ltle 10718 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶𝐴𝐶))
653adant2 1123 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶𝐴𝐶))
74, 6syld 47 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴𝐶))
87expdimp 453 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵 < 𝐶𝐴𝐶))
9 breq2 5062 . . . . . 6 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
109biimpcd 250 . . . . 5 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
1110adantl 482 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵 = 𝐶𝐴𝐶))
128, 11jaod 853 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → ((𝐵 < 𝐶𝐵 = 𝐶) → 𝐴𝐶))
133, 12sylbid 241 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵𝐶𝐴𝐶))
1413expimpd 454 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105   class class class wbr 5058  cr 10525   < clt 10664  cle 10665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670
This theorem is referenced by:  letri  10758  letrd  10786  le2add  11111  le2sub  11128  p1le  11474  lemul12b  11486  lemul12a  11487  zletr  12015  peano2uz2  12059  ledivge1le  12450  lemaxle  12578  elfz1b  12966  elfz0fzfz0  13002  fz0fzelfz0  13003  fz0fzdiffz0  13006  elfzmlbp  13008  difelfznle  13011  elincfzoext  13085  ssfzoulel  13121  ssfzo12bi  13122  flge  13165  flflp1  13167  fldiv4p1lem1div2  13195  fldiv4lem1div2uz2  13196  monoord  13390  le2sq2  13490  leexp2r  13528  expubnd  13531  facwordi  13639  faclbnd3  13642  facavg  13651  fi1uzind  13845  swrdswrdlem  14056  swrdccat  14087  sqrlem1  14592  sqrlem6  14597  sqrlem7  14598  leabs  14649  limsupbnd2  14830  rlim3  14845  lo1bdd2  14871  lo1bddrp  14872  o1lo1  14884  lo1mul  14974  lo1le  14998  isercolllem2  15012  iseraltlem2  15029  fsumabs  15146  cvgrat  15229  ruclem9  15581  algcvga  15913  prmdvdsfz  16039  prmfac1  16053  eulerthlem2  16109  modprm0  16132  prmreclem1  16242  prmreclem4  16245  4sqlem11  16281  vdwnnlem3  16323  gsumbagdiaglem  20085  zntoslem  20633  cnllycmp  23489  evth  23492  ovoliunlem2  24033  ovolicc2lem3  24049  itg2monolem1  24280  coeaddlem  24768  coemullem  24769  aalioulem5  24854  aalioulem6  24855  sincosq1lem  25012  emcllem6  25506  ftalem3  25580  fsumvma2  25718  chpchtsum  25723  bcmono  25781  bposlem5  25792  gausslemma2dlem1a  25869  lgsquadlem1  25884  dchrisum0lem1  26020  pntrsumbnd2  26071  pntleml  26115  brbtwn2  26619  axlowdimlem17  26672  axlowdim  26675  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  wwlksubclwwlk  27765  eupth2lems  27945  nmoub3i  28478  ubthlem1  28575  ubthlem2  28576  nmopub2tALT  29614  nmfnleub2  29631  lnconi  29738  leoptr  29842  pjnmopi  29853  cdj3lem2b  30142  eulerpartlemb  31526  isbasisrelowllem1  34519  isbasisrelowllem2  34520  ltflcei  34762  itg2addnclem2  34826  itg2addnclem3  34827  itg2addnc  34828  bddiblnc  34844  dvasin  34860  incsequz  34906  mettrifi  34915  equivbnd  34951  bfplem1  34983  jm2.17b  39438  fmul01lt1lem2  41746  eluzge0nn0  43393  elfz2z  43396  iccpartiltu  43429  iccpartgt  43434  lighneallem2  43618
  Copyright terms: Public domain W3C validator