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

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

Proof of Theorem letr
StepHypRef Expression
1 leloe 11246 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
213adant1 1131 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
32adantr 482 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
4 lelttr 11250 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
5 ltle 11248 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶𝐴𝐶))
653adant2 1132 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶𝐴𝐶))
74, 6syld 47 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴𝐶))
87expdimp 454 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵 < 𝐶𝐴𝐶))
9 breq2 5110 . . . . . 6 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
109biimpcd 249 . . . . 5 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
1110adantl 483 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵 = 𝐶𝐴𝐶))
128, 11jaod 858 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → ((𝐵 < 𝐶𝐵 = 𝐶) → 𝐴𝐶))
133, 12sylbid 239 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵𝐶𝐴𝐶))
1413expimpd 455 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107   class class class wbr 5106  cr 11055   < clt 11194  cle 11195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11113  ax-pre-lttri 11130  ax-pre-lttrn 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200
This theorem is referenced by:  letri  11289  letrd  11317  le2add  11642  le2sub  11659  p1le  12005  lemul12b  12017  lemul12a  12018  zletr  12552  peano2uz2  12596  ledivge1le  12991  lemaxle  13120  elfz1b  13516  elfz0fzfz0  13552  fz0fzelfz0  13553  fz0fzdiffz0  13556  elfzmlbp  13558  difelfznle  13561  elincfzoext  13636  ssfzoulel  13672  ssfzo12bi  13673  flge  13716  flflp1  13718  fldiv4p1lem1div2  13746  fldiv4lem1div2uz2  13747  monoord  13944  le2sq2  14046  leexp2r  14085  expubnd  14088  facwordi  14195  faclbnd3  14198  facavg  14207  fi1uzind  14402  swrdswrdlem  14598  swrdccat  14629  01sqrexlem1  15133  01sqrexlem6  15138  01sqrexlem7  15139  leabs  15190  limsupbnd2  15371  rlim3  15386  lo1bdd2  15412  lo1bddrp  15413  o1lo1  15425  lo1mul  15516  lo1le  15542  isercolllem2  15556  iseraltlem2  15573  fsumabs  15691  cvgrat  15773  ruclem9  16125  algcvga  16460  prmdvdsfz  16586  prmfac1  16602  eulerthlem2  16659  modprm0  16682  prmreclem1  16793  prmreclem4  16796  4sqlem11  16832  vdwnnlem3  16874  zntoslem  20979  gsumbagdiaglemOLD  21356  gsumbagdiaglem  21359  cnllycmp  24335  evth  24338  ovoliunlem2  24883  ovolicc2lem3  24899  itg2monolem1  25131  bddiblnc  25222  coeaddlem  25626  coemullem  25627  aalioulem5  25712  aalioulem6  25713  sincosq1lem  25870  emcllem6  26366  ftalem3  26440  fsumvma2  26578  chpchtsum  26583  bcmono  26641  bposlem5  26652  gausslemma2dlem1a  26729  lgsquadlem1  26744  dchrisum0lem1  26880  pntrsumbnd2  26931  pntleml  26975  brbtwn2  27896  axlowdimlem17  27949  axlowdim  27952  crctcshwlkn0lem3  28799  crctcshwlkn0lem5  28801  wwlksubclwwlk  29044  eupth2lems  29224  nmoub3i  29757  ubthlem1  29854  ubthlem2  29855  nmopub2tALT  30893  nmfnleub2  30910  lnconi  31017  leoptr  31121  pjnmopi  31132  cdj3lem2b  31421  eulerpartlemb  33025  isbasisrelowllem1  35872  isbasisrelowllem2  35873  ltflcei  36112  itg2addnclem2  36176  itg2addnclem3  36177  itg2addnc  36178  dvasin  36208  incsequz  36253  mettrifi  36262  equivbnd  36295  bfplem1  36327  jm2.17b  41328  fmul01lt1lem2  43912  eluzge0nn0  45630  elfz2z  45633  iccpartiltu  45700  iccpartgt  45705  lighneallem2  45884
  Copyright terms: Public domain W3C validator