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

Theorem ltletr 10352
Description: Transitive law. (Contributed by NM, 25-Aug-1999.)
Assertion
Ref Expression
ltletr ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))

Proof of Theorem ltletr
StepHypRef Expression
1 leloe 10347 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
213adant1 1151 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 ↔ (𝐵 < 𝐶𝐵 = 𝐶)))
3 lttr 10337 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
43expcomd 403 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 → (𝐴 < 𝐵𝐴 < 𝐶)))
5 breq2 4801 . . . . . . 7 (𝐵 = 𝐶 → (𝐴 < 𝐵𝐴 < 𝐶))
65biimpd 220 . . . . . 6 (𝐵 = 𝐶 → (𝐴 < 𝐵𝐴 < 𝐶))
76a1i 11 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 = 𝐶 → (𝐴 < 𝐵𝐴 < 𝐶)))
84, 7jaod 875 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 < 𝐶𝐵 = 𝐶) → (𝐴 < 𝐵𝐴 < 𝐶)))
92, 8sylbid 231 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵𝐶 → (𝐴 < 𝐵𝐴 < 𝐶)))
109com23 86 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐵𝐶𝐴 < 𝐶)))
1110impd 397 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383  wo 863  w3a 1098   = wceq 1634  wcel 2148   class class class wbr 4797  cr 10158   < clt 10297  cle 10298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-resscn 10216  ax-pre-lttri 10233  ax-pre-lttrn 10234
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-er 7917  df-en 8131  df-dom 8132  df-sdom 8133  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303
This theorem is referenced by:  ltleletr  10353  ltletri  10388  ltletrd  10420  ltleadd  10734  lediv12a  11139  nngt0  11272  nnrecgt0  11281  elnnnn0c  11562  elnnz1  11627  zltp1le  11651  uz3m2nn  11955  zbtwnre  12011  ledivge1le  12121  addlelt  12164  qbtwnre  12254  xlemul1a  12342  xrsupsslem  12361  zltaddlt1le  12553  elfzodifsumelfzo  12764  ssfzo12bi  12793  elfznelfzo  12803  ceile  12878  swrdswrd  13691  swrdccatin1  13714  repswswrd  13762  sqrlem4  14216  resqrex  14221  caubnd  14328  rlim2lt  14458  cos01gt0  15149  znnenlem  15168  ruclem12  15198  oddge22np1  15303  sadcaddlem  15408  nn0seqcvgd  15512  coprm  15650  prmgaplem7  15988  prmlem1  16041  prmlem2  16054  icoopnst  22978  ovollb2lem  23496  dvcnvrelem1  24021  aaliou  24334  tanord  24526  logdivlti  24608  logdivlt  24609  ftalem2  25042  gausslemma2dlem1a  25332  pntlem3  25540  crctcshwlkn0lem3  26961  nn0prpwlem  32671  isbasisrelowllem1  33557  isbasisrelowllem2  33558  ltflcei  33747  tan2h  33751  poimirlem29  33788  poimirlem32  33791  stoweidlem26  40766  stoweid  40803  2leaddle2  41864  pfx2  41964  gbegt5  42201  gbowgt5  42202  sgoldbeven3prm  42223  nnsum4primesodd  42236  nnsum4primesoddALTV  42237  evengpoap3  42239  bgoldbnnsum3prm  42244  cznnring  42508  nn0sumltlt  42680  rege1logbrege0  42904  rege1logbzge0  42905  fllog2  42914  dignn0ldlem  42948
  Copyright terms: Public domain W3C validator