Theorem lttr 11220

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

Assertion

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

Proof of Theorem lttr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035   < clt 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182

This theorem is referenced by:  ltso  11224  lelttr  11234  ltletr  11236  lttri  11270  lttrd  11305  lt2sub  11646  mulgt1OLD  12012  recgt1i  12051  recreclt  12053  sup2  12110  nnge1  12203  recnz  12602  gtndiv  12604  xrlttr  13089  fzo1fzo0n0  13668  flflp1  13764  1mod  13860  seqf1olem1  14001  expnbnd  14192  expnlbnd  14193  swrd2lsw  14912  2swrd2eqwrdeq  14913  sin01gt0  16155  cos01gt0  16156  p1modz1  16226  ltoddhalfle  16328  nno  16349  dvdsnprmd  16657  chfacfscmul0  22848  chfacfpmmul0  22852  iscmet3lem1  25283  bcthlem4  25319  bcthlem5  25320  ivthlem2  25444  ovolicc2lem3  25511  mbfaddlem  25652  reeff1olem  26436  logdivlti  26609  ftalem2  27062  chtub  27200  bclbnd  27268  efexple  27269  bposlem1  27272  lgsquadlem2  27369  pntlem3  27597  axlowdimlem16  29051  pthdlem1  29859  wwlksnredwwlkn  29988  clwwlkel  30141  clwwlknonex2lem2  30203  frgrogt3nreg  30492  poimirlem2  37996  sn-sup2  42988  stoweidlem34  46484  m1mod0mod1  47830  smonoord  47847  muldvdsfacgt  47856  muldvdsfacm1  47857  sbgoldbalt  48279  bgoldbtbndlem3  48305  bgoldbtbndlem4  48306  tgoldbach  48315  regt1loggt0  49034  rege1logbrege0  49056  dignn0flhalflem1  49113