Theorem lttr 11250

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

Assertion

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

Proof of Theorem lttr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   < clt 11208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttrn 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  ltso  11254  lelttr  11264  ltletr  11266  lttri  11300  lttrd  11335  lt2sub  11676  mulgt1OLD  12041  recgt1i  12080  recreclt  12082  sup2  12139  nnge1  12214  recnz  12609  gtndiv  12611  xrlttr  13100  fzo1fzo0n0  13676  flflp1  13769  1mod  13865  seqf1olem1  14006  expnbnd  14197  expnlbnd  14198  swrd2lsw  14918  2swrd2eqwrdeq  14919  sin01gt0  16158  cos01gt0  16159  p1modz1  16229  ltoddhalfle  16331  nno  16352  dvdsnprmd  16660  chfacfscmul0  22745  chfacfpmmul0  22749  iscmet3lem1  25191  bcthlem4  25227  bcthlem5  25228  ivthlem2  25353  ovolicc2lem3  25420  mbfaddlem  25561  reeff1olem  26356  logdivlti  26529  ftalem2  26984  chtub  27123  bclbnd  27191  efexple  27192  bposlem1  27195  lgsquadlem2  27292  pntlem3  27520  axlowdimlem16  28884  pthdlem1  29696  wwlksnredwwlkn  29825  clwwlkel  29975  clwwlknonex2lem2  30037  frgrogt3nreg  30326  poimirlem2  37616  sn-sup2  42479  stoweidlem34  46032  m1mod0mod1  47355  smonoord  47372  sbgoldbalt  47782  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  tgoldbach  47818  regt1loggt0  48525  rege1logbrege0  48547  dignn0flhalflem1  48604