MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lelttr Unicode version

Theorem lelttr 8928
Description: Transitive law. (Contributed by NM, 23-May-1999.)
Assertion
Ref Expression
lelttr  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )

Proof of Theorem lelttr
StepHypRef Expression
1 leloe 8924 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <_  B  <->  ( A  <  B  \/  A  =  B )
) )
213adant3 975 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <_  B  <->  ( A  <  B  \/  A  =  B ) ) )
3 lttr 8915 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <  B  /\  B  <  C )  ->  A  <  C
) )
43exp3a 425 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <  B  ->  ( B  <  C  ->  A  <  C ) ) )
5 breq1 4042 . . . . . 6  |-  ( A  =  B  ->  ( A  <  C  <->  B  <  C ) )
65biimprd 214 . . . . 5  |-  ( A  =  B  ->  ( B  <  C  ->  A  <  C ) )
76a1i 10 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  =  B  ->  ( B  <  C  ->  A  <  C ) ) )
84, 7jaod 369 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <  B  \/  A  =  B
)  ->  ( B  <  C  ->  A  <  C ) ) )
92, 8sylbid 206 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <_  B  ->  ( B  <  C  ->  A  <  C ) ) )
109imp3a 420 1  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696   class class class wbr 4039   RRcr 8752    < clt 8883    <_ cle 8884
This theorem is referenced by:  letr  8930  lelttri  8962  lelttrd  8990  letrp1  9614  ltmul12a  9628  ledivp1  9674  supmul1  9735  bndndx  9980  uzind  10119  fnn0ind  10127  rpnnen1lem5  10362  xrinfmsslem  10642  flge  10953  fsequb  11053  expnlbnd2  11248  caubnd2  11857  caubnd  11858  mulcn2  12085  cn1lem  12087  rlimo1  12106  o1rlimmul  12108  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  climsup  12159  caucvgrlem2  12163  iseralt  12173  cvgcmp  12290  cvgcmpce  12292  ruclem3  12527  ruclem12  12535  algcvgblem  12763  pclem  12907  infpn2  12976  metss2lem  18073  ngptgp  18168  nghmcn  18270  iocopnst  18454  ovollb2lem  18863  ovolicc2lem4  18895  volcn  18977  ismbf3d  19025  dvcnvrelem1  19380  dvfsumrlim  19394  ulmcn  19792  mtest  19797  logdivlti  19987  isosctrlem1  20134  ftalem2  20327  chtub  20467  bposlem6  20544  chtppilim  20640  dchrisumlem3  20656  pntlem3  20774  vacn  21283  nmcvcn  21284  blocni  21399  chscllem2  22233  lnconi  22629  staddi  22842  stadd3i  22844  bcm1n  23048  ltflcei  24998  lxflflp1  25000  geomcau  26578  heibor1lem  26636  bfplem2  26650  rrncmslem  26659  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climinf  27835  stoweidlem5  27857  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem25  27877  stoweidlem26  27878  stoweidlem42  27894  stoweidlem59  27911  stoweid  27915  wallispilem3  27919  wallispilem4  27920  wallispilem5  27921  nvnencycllem  28389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-resscn 8810  ax-pre-lttri 8827  ax-pre-lttrn 8828
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889
  Copyright terms: Public domain W3C validator