Theorem lttr 9864

Description: Alias for axlttrn 9860, for naming consistency with lttri 9914. New proofs should generally use this instead of ax-pre-lttrn 9766. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
lttr	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Proof of Theorem lttr

Step	Hyp	Ref	Expression
1		axlttrn 9860	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030   ∈ wcel 1938   class class class wbr 4481  ℝcr 9690   < clt 9829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-resscn 9748  ax-pre-lttrn 9766

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-er 7505  df-en 7718  df-dom 7719  df-sdom 7720  df-pnf 9831  df-mnf 9832  df-ltxr 9834

This theorem is referenced by:  ltso  9868  lelttr  9878  ltletr  9879  lttri  9914  lttrd  9949  lt2sub  10275  mulgt1  10631  recgt1i  10670  recreclt  10672  sup2  10732  nnge1  10801  recnz  11192  gtndiv  11194  xrlttr  11718  fzo1fzo0n0  12254  flflp1  12338  1mod  12432  seqf1olem1  12570  expnbnd  12723  expnlbnd  12724  swrd2lsw  13402  2swrd2eqwrdeq  13403  sin01gt0  14628  cos01gt0  14629  ltoddhalfle  14792  nno  14805  dvdsnprmd  15117  chfacfscmul0  20385  chfacfpmmul0  20389  iscmet3lem1  22761  bcthlem4  22795  bcthlem5  22796  ivthlem2  22903  ovolicc2lem3  22969  mbfaddlem  23108  reeff1olem  23891  logdivlti  24057  logblog  24217  ftalem2  24487  chtub  24626  bclbnd  24694  efexple  24695  bposlem1  24698  lgsquadlem2  24795  pntlem3  24987  axlowdimlem16  25527  wwlknredwwlkn  25992  clwwlkel  26059  numclwwlkovf2ex  26351  frgraogt3nreg  26385  poimirlem2  32471  stoweidlem34  38830  smonoord  39852  m1mod0mod1  39857  sgoldbalt  40111  bgoldbtbndlem3  40131  bgoldbtbndlem4  40132  tgoldbach  40140  tgoldbachOLD  40147  pthdlem1  41077  wwlksnredwwlkn  41206  clwwlksel  41326  av-numclwwlkovf2ex  41622  av-frgraogt3nreg  41656  difmodm1lt  42216  regt1loggt0  42233  rege1logbrege0  42255  dignn0flhalflem1  42312