Theorem lttr 10326

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

Assertion

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

Proof of Theorem lttr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   ∈ wcel 2139   class class class wbr 4804  ℝcr 10147   < clt 10286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-resscn 10205  ax-pre-lttrn 10223

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-pnf 10288  df-mnf 10289  df-ltxr 10291

This theorem is referenced by:  ltso  10330  lelttr  10340  ltletr  10341  lttri  10375  lttrd  10410  lt2sub  10738  mulgt1  11094  recgt1i  11132  recreclt  11134  sup2  11191  nnge1  11258  recnz  11664  gtndiv  11666  xrlttr  12186  fzo1fzo0n0  12733  flflp1  12822  1mod  12916  seqf1olem1  13054  expnbnd  13207  expnlbnd  13208  swrd2lsw  13916  2swrd2eqwrdeq  13917  sin01gt0  15139  cos01gt0  15140  p1modz1  15209  ltoddhalfle  15307  nno  15320  dvdsnprmd  15625  chfacfscmul0  20885  chfacfpmmul0  20889  iscmet3lem1  23309  bcthlem4  23344  bcthlem5  23345  ivthlem2  23441  ovolicc2lem3  23507  mbfaddlem  23646  reeff1olem  24419  logdivlti  24586  logblog  24750  ftalem2  25020  chtub  25157  bclbnd  25225  efexple  25226  bposlem1  25229  lgsquadlem2  25326  pntlem3  25518  axlowdimlem16  26057  pthdlem1  26893  wwlksnredwwlkn  27034  clwwlkel  27196  clwwlknonex2lem2  27278  frgrogt3nreg  27586  poimirlem2  33742  stoweidlem34  40772  m1mod0mod1  41867  smonoord  41869  sbgoldbalt  42197  bgoldbtbndlem3  42223  bgoldbtbndlem4  42224  tgoldbach  42233  tgoldbachOLD  42240  difmodm1lt  42845  regt1loggt0  42858  rege1logbrege0  42880  dignn0flhalflem1  42937