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

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

Proof of Theorem letr
StepHypRef Expression
1 leloe 10412 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
213adant1 1153 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
32adantr 468 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
4 lelttr 10416 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
5 ltle 10414 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶𝐴𝐶))
653adant2 1154 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐶𝐴𝐶))
74, 6syld 47 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴𝐶))
87expdimp 442 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵 < 𝐶𝐴𝐶))
9 breq2 4855 . . . . . 6 (𝐵 = 𝐶 → (𝐴𝐵𝐴𝐶))
109biimpcd 240 . . . . 5 (𝐴𝐵 → (𝐵 = 𝐶𝐴𝐶))
1110adantl 469 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵 = 𝐶𝐴𝐶))
128, 11jaod 877 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → ((𝐵 < 𝐶𝐵 = 𝐶) → 𝐴𝐶))
133, 12sylbid 231 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴𝐵) → (𝐵𝐶𝐴𝐶))
1413expimpd 443 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2157   class class class wbr 4851  cr 10223   < clt 10362  cle 10363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-resscn 10281  ax-pre-lttri 10298  ax-pre-lttrn 10299
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368
This theorem is referenced by:  letri  10454  letrd  10482  le2add  10798  le2sub  10815  p1le  11154  lemul12b  11168  lemul12a  11169  zletr  11690  peano2uz2  11734  ledivge1le  12118  lemaxle  12247  elfz1b  12635  elfz0fzfz0  12671  fz0fzelfz0  12672  fz0fzdiffz0  12675  elfzmlbp  12677  difelfznle  12680  elincfzoext  12753  ssfzoulel  12789  ssfzo12bi  12790  flge  12833  flflp1  12835  fldiv4p1lem1div2  12863  fldiv4lem1div2uz2  12864  monoord  13057  leexp2r  13144  expubnd  13147  le2sq2  13165  facwordi  13299  faclbnd3  13302  facavg  13311  fi1uzind  13499  swrdswrdlem  13686  swrdccat  13720  sqrlem1  14209  sqrlem6  14214  sqrlem7  14215  leabs  14265  limsupbnd2  14440  rlim3  14455  lo1bdd2  14481  lo1bddrp  14482  o1lo1  14494  lo1mul  14584  lo1le  14608  isercolllem2  14622  iseraltlem2  14639  fsumabs  14758  cvgrat  14839  ruclem9  15190  algcvga  15514  prmdvdsfz  15637  prmfac1  15651  eulerthlem2  15707  modprm0  15730  prmreclem1  15840  prmreclem4  15843  4sqlem11  15879  vdwnnlem3  15921  gsumbagdiaglem  19587  zntoslem  20115  cnllycmp  22972  evth  22975  ovoliunlem2  23490  ovolicc2lem3  23506  itg2monolem1  23737  coeaddlem  24225  coemullem  24226  aalioulem5  24311  aalioulem6  24312  sincosq1lem  24470  emcllem6  24947  ftalem3  25021  fsumvma2  25159  chpchtsum  25164  bcmono  25222  bposlem5  25233  gausslemma2dlem1a  25310  lgsquadlem1  25325  dchrisum0lem1  25425  pntrsumbnd2  25476  pntleml  25520  brbtwn2  26005  axlowdimlem17  26058  axlowdim  26061  crctcshwlkn0lem3  26939  crctcshwlkn0lem5  26941  wwlksubclwwlk  27215  clwlksfclwwlkOLD  27242  eupth2lems  27417  nmoub3i  27962  ubthlem1  28060  ubthlem2  28061  nmopub2tALT  29102  nmfnleub2  29119  lnconi  29226  leoptr  29330  pjnmopi  29341  cdj3lem2b  29630  eulerpartlemb  30761  isbasisrelowllem1  33521  isbasisrelowllem2  33522  ltflcei  33712  itg2addnclem2  33776  itg2addnclem3  33777  itg2addnc  33778  bddiblnc  33794  dvasin  33810  incsequz  33857  mettrifi  33866  equivbnd  33902  bfplem1  33934  jm2.17b  38030  fmul01lt1lem2  40298  eluzge0nn0  41898  elfz2z  41901  iccpartiltu  41934  iccpartgt  41939  lighneallem2  42099
  Copyright terms: Public domain W3C validator