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

Theorem lelttr 11246
Description: Transitive law. (Contributed by NM, 23-May-1999.)
Assertion
Ref Expression
lelttr ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Proof of Theorem lelttr
StepHypRef Expression
1 leloe 11242 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
213adant3 1133 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))
3 lttr 11232 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
43expd 417 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐵 < 𝐶𝐴 < 𝐶)))
5 breq1 5109 . . . . . 6 (𝐴 = 𝐵 → (𝐴 < 𝐶𝐵 < 𝐶))
65biimprd 248 . . . . 5 (𝐴 = 𝐵 → (𝐵 < 𝐶𝐴 < 𝐶))
76a1i 11 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 = 𝐵 → (𝐵 < 𝐶𝐴 < 𝐶)))
84, 7jaod 858 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐴 = 𝐵) → (𝐵 < 𝐶𝐴 < 𝐶)))
92, 8sylbid 239 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴𝐵 → (𝐵 < 𝐶𝐴 < 𝐶)))
109impd 412 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 11051   < clt 11190  cle 11191
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 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-pre-lttri 11126  ax-pre-lttrn 11127
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  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 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196
This theorem is referenced by:  leltletr  11247  letr  11250  lelttri  11283  lelttrd  11314  letrp1  12000  ltmul12a  12012  ledivp1  12058  supmul1  12125  bndndx  12413  uzind  12596  fnn0ind  12603  rpnnen1lem5  12907  xrinfmsslem  13228  elfzo0z  13615  nn0p1elfzo  13616  fzofzim  13620  elfzodifsumelfzo  13639  flge  13711  flflp1  13713  flltdivnn0lt  13739  modfzo0difsn  13849  fsequb  13881  expnlbnd2  14138  ccat2s1fvw  14527  swrdswrd  14594  pfxccatin12lem3  14621  repswswrd  14673  caubnd2  15243  caubnd  15244  mulcn2  15479  cn1lem  15481  rlimo1  15500  o1rlimmul  15502  climsqz  15524  climsqz2  15525  rlimsqzlem  15534  climsup  15555  caucvgrlem2  15560  iseralt  15570  cvgcmp  15702  cvgcmpce  15704  ruclem3  16116  ruclem12  16124  ltoddhalfle  16244  algcvgblem  16454  ncoprmlnprm  16604  pclem  16711  infpn2  16786  gsummoncoe1  21678  mp2pm2mplem4  22161  metss2lem  23870  ngptgp  23995  nghmcn  24112  iocopnst  24306  ovollb2lem  24855  ovolicc2lem4  24887  volcn  24973  ismbf3d  25021  dvcnvrelem1  25384  dvfsumrlim  25398  ulmcn  25761  mtest  25766  logdivlti  25978  isosctrlem1  26171  ftalem2  26426  chtub  26563  bposlem6  26640  gausslemma2dlem2  26718  chtppilim  26826  dchrisumlem3  26842  pntlem3  26960  clwlkclwwlklem2a  28945  vacn  29639  nmcvcn  29640  blocni  29750  chscllem2  30583  lnconi  30978  staddi  31191  stadd3i  31193  ltflcei  36069  poimirlem29  36110  geomcau  36221  heibor1lem  36271  bfplem2  36285  rrncmslem  36294  climinf  43854  zm1nn  45541  iccpartigtl  45622  tgoldbach  46016  ply1mulgsumlem2  46475  difmodm1lt  46615
  Copyright terms: Public domain W3C validator