Theorem lttr 9741

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

Assertion

Ref	Expression
lttr	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )

Proof of Theorem lttr

Step	Hyp	Ref	Expression
1		axlttrn 9737	1 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991   e. wcel 1898   class class class wbr 4418   RRcr 9569   < clt 9706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-pre-lttrn 9645

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-ltxr 9711

This theorem is referenced by:  ltso  9745  lelttr  9755  ltletr  9756  lttri  9791  lttrd  9827  lt2sub  10145  mulgt1  10497  recgt1i  10536  recreclt  10538  sup2  10598  nnge1  10668  recnz  11045  gtndiv  11047  xrlttr  11473  fzo1fzo0n0  11994  flflp1  12081  1mod  12167  seqf1olem1  12290  expnbnd  12439  expnlbnd  12440  swrd2lsw  13082  2swrd2eqwrdeq  13083  sin01gt0  14299  cos01gt0  14300  chfacfscmul0  19937  chfacfpmmul0  19941  iscmet3lem1  22316  bcthlem4  22350  bcthlem5  22351  ivthlem2  22458  ovolicc2lem3  22527  mbfaddlem  22672  reeff1olem  23457  logdivlti  23625  logblog  23785  ftalem2  24054  chtub  24196  bclbnd  24264  efexple  24265  bposlem1  24268  lgsquadlem2  24339  pntlem3  24503  axlowdimlem16  25043  wwlknredwwlkn  25510  clwwlkel  25577  numclwwlkovf2ex  25870  frgraogt3nreg  25904  poimirlem2  31988  stoweidlem34  37996  smonoord  38853  m1mod0mod1  38858  sgoldbalt  39017  bgoldbtbndlem3  39037  bgoldbtbndlem4  39038  tgoldbach  39046  pthdlem1  39888  difmodm1lt  40694  nno  40697  regt1loggt0  40716  rege1logbrege0  40738  dignn0flhalflem1  40795