Theorem lttr 11413

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

Assertion

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

Proof of Theorem lttr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2147   class class class wbr 5106  ℝcr 11226   < clt 11370

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-pre-lttrn 11302

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375

This theorem is used by:  ltso  11417  lelttr  11427  ltletr  11429  lttri  11463  lttrd  11498  lt2sub  11841  recgt1i  12241  recreclt  12243  sup2  12300  nnge1  12393  recnz  12801  gtndiv  12803  xrlttr  13296  fzo1fzo0n0  13877  flflp1  13974  1mod  14070  seqf1olem1  14211  expnbnd  14403  expnlbnd  14404  swrd2lsw  15134  2swrd2eqwrdeq  15135  sin01gt0  16387  cos01gt0  16388  p1modz1  16458  ltoddhalfle  16560  nno  16581  dvdsnprmd  16894  chfacfscmul0  23206  chfacfpmmul0  23210  iscmet3lem1  25642  bcthlem4  25678  bcthlem5  25679  ivthlem2  25803  ovolicc2lem3  25870  mbfaddlem  26011  reeff1olem  26803  logdivlti  26978  ftalem2  27431  chtub  27569  bclbnd  27637  efexple  27638  bposlem1  27641  lgsquadlem2  27738  pntlem3  27966  axlowdimlem16  29565  pthdlem1  30382  wwlksnredwwlkn  30514  clwwlkel  30667  clwwlknonex2lem2  30729  frgrogt3nreg  31028  poimirlem2  38732  sn-sup2  43748  stoweidlem34  47249  m1mod0mod1  48635  smonoord  48652  muldvdsfacgt  48661  muldvdsfacm1  48662  sbgoldbalt  49084  bgoldbtbndlem3  49110  bgoldbtbndlem4  49111  tgoldbach  49120  regt1loggt0  49853  rege1logbrege0  49875  dignn0flhalflem1  49932