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

Theorem lelttr 8912
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 8908 . . . 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 8899 . . . . 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 4026 . . . . . 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 1623    e. wcel 1684   class class class wbr 4023   RRcr 8736    < clt 8867    <_ cle 8868
This theorem is referenced by:  letr  8914  lelttri  8946  lelttrd  8974  letrp1  9598  ltmul12a  9612  ledivp1  9658  supmul1  9719  bndndx  9964  uzind  10103  fnn0ind  10111  rpnnen1lem5  10346  xrinfmsslem  10626  flge  10937  fsequb  11037  expnlbnd2  11232  caubnd2  11841  caubnd  11842  mulcn2  12069  cn1lem  12071  rlimo1  12090  o1rlimmul  12092  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  climsup  12143  caucvgrlem2  12147  iseralt  12157  cvgcmp  12274  cvgcmpce  12276  ruclem3  12511  ruclem12  12519  algcvgblem  12747  pclem  12891  infpn2  12960  metss2lem  18057  ngptgp  18152  nghmcn  18254  iocopnst  18438  ovollb2lem  18847  ovolicc2lem4  18879  volcn  18961  ismbf3d  19009  dvcnvrelem1  19364  dvfsumrlim  19378  ulmcn  19776  mtest  19781  logdivlti  19971  isosctrlem1  20118  ftalem2  20311  chtub  20451  bposlem6  20528  chtppilim  20624  dchrisumlem3  20640  pntlem3  20758  vacn  21267  nmcvcn  21268  blocni  21383  chscllem2  22217  lnconi  22613  staddi  22826  stadd3i  22828  bcm1n  23032  geomcau  25887  heibor1lem  25945  bfplem2  25959  rrncmslem  25968  fmul01lt1lem1  27126  fmul01lt1lem2  27127  climinf  27144  stoweidlem5  27166  stoweidlem11  27172  stoweidlem13  27174  stoweidlem14  27175  stoweidlem25  27186  stoweidlem26  27187  stoweidlem42  27203  stoweidlem59  27220  stoweid  27224  wallispilem3  27228  wallispilem4  27229  wallispilem5  27230
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8794  ax-pre-lttri 8811  ax-pre-lttrn 8812
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873
  Copyright terms: Public domain W3C validator