Theorem lttr 10114

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

Assertion

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

Proof of Theorem lttr

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037   ∈ wcel 1990   class class class wbr 4653  ℝcr 9935   < clt 10074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079

This theorem is referenced by:  ltso  10118  lelttr  10128  ltletr  10129  lttri  10163  lttrd  10198  lt2sub  10526  mulgt1  10882  recgt1i  10920  recreclt  10922  sup2  10979  nnge1  11046  recnz  11452  gtndiv  11454  xrlttr  11973  fzo1fzo0n0  12518  flflp1  12608  1mod  12702  seqf1olem1  12840  expnbnd  12993  expnlbnd  12994  swrd2lsw  13695  2swrd2eqwrdeq  13696  sin01gt0  14920  cos01gt0  14921  ltoddhalfle  15085  nno  15098  dvdsnprmd  15403  chfacfscmul0  20663  chfacfpmmul0  20667  iscmet3lem1  23089  bcthlem4  23124  bcthlem5  23125  ivthlem2  23221  ovolicc2lem3  23287  mbfaddlem  23427  reeff1olem  24200  logdivlti  24366  logblog  24530  ftalem2  24800  chtub  24937  bclbnd  25005  efexple  25006  bposlem1  25009  lgsquadlem2  25106  pntlem3  25298  axlowdimlem16  25837  pthdlem1  26662  wwlksnredwwlkn  26790  clwwlksel  26914  numclwwlkovf2exlem2  27212  frgrogt3nreg  27255  poimirlem2  33411  stoweidlem34  40251  m1mod0mod1  41339  smonoord  41341  sbgoldbalt  41669  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  tgoldbach  41705  tgoldbachOLD  41712  difmodm1lt  42317  regt1loggt0  42330  rege1logbrege0  42352  dignn0flhalflem1  42409