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

Theorem letr 9460
Description: Transitive law. (Contributed by NM, 12-Nov-1999.)
Assertion
Ref Expression
letr  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )

Proof of Theorem letr
StepHypRef Expression
1 leloe 9453 . . . . 5  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C )
) )
213adant1 1006 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C ) ) )
32adantr 465 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  <_  C 
<->  ( B  <  C  \/  B  =  C
) ) )
4 lelttr 9457 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
5 ltle 9455 . . . . . . 7  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A  <  C  ->  A  <_  C )
)
653adant2 1007 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <  C  ->  A  <_  C ) )
74, 6syld 44 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <_  C
) )
87expdimp 437 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  < 
C  ->  A  <_  C ) )
9 breq2 4291 . . . . . 6  |-  ( B  =  C  ->  ( A  <_  B  <->  A  <_  C ) )
109biimpcd 224 . . . . 5  |-  ( A  <_  B  ->  ( B  =  C  ->  A  <_  C ) )
1110adantl 466 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  =  C  ->  A  <_  C ) )
128, 11jaod 380 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( ( B  <  C  \/  B  =  C )  ->  A  <_  C ) )
133, 12sylbid 215 . 2  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  <_  C  ->  A  <_  C
) )
1413expimpd 603 1  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <_  C )  ->  A  <_  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   class class class wbr 4287   RRcr 9273    < clt 9410    <_ cle 9411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-pre-lttri 9348  ax-pre-lttrn 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416
This theorem is referenced by:  letri  9495  letrd  9520  le2add  9813  le2sub  9830  p1le  10164  lemul12b  10178  lemul12a  10179  zletr  10681  peano2uz2  10721  uzletr  10861  uztrn  10869  uzss  10873  elfz0fzfz0  11477  fz0fzelfz0  11478  fz0fzdiffz0  11481  elfzmlbm  11482  elfzmlbp  11483  elfz1b  11519  ssfzoulel  11613  ssfzo12bi  11614  flge  11647  monoord  11828  leexp2r  11913  expubnd  11916  le2sq2  11933  facwordi  12057  faclbnd3  12060  facavg  12069  brfi1uzind  12211  swrdswrdlem  12345  swrdccat  12376  sqrlem1  12724  sqrlem6  12729  sqrlem7  12730  leabs  12780  limsupbnd2  12953  rlim3  12968  lo1bdd2  12994  lo1bddrp  12995  o1lo1  13007  lo1mul  13097  lo1le  13121  isercolllem2  13135  iseraltlem2  13152  fsumabs  13256  cvgrat  13335  ruclem9  13512  algcvga  13746  prmfac1  13796  eulerthlem2  13849  modprm0  13865  prmreclem1  13969  prmreclem4  13972  4sqlem11  14008  vdwnnlem3  14050  gsumbagdiaglem  17422  zntoslem  17964  cnllycmp  20503  evth  20506  ovoliunlem2  20961  ovolicc2lem3  20977  itg2monolem1  21203  coeaddlem  21691  coemullem  21692  aalioulem5  21777  aalioulem6  21778  sincosq1lem  21934  emcllem6  22369  ftalem3  22387  fsumvma2  22528  chpchtsum  22533  bcmono  22591  bposlem5  22602  lgsquadlem1  22668  dchrisum0lem1  22740  pntrsumbnd2  22791  pntleml  22835  brbtwn2  23102  axlowdimlem17  23155  axlowdim  23158  eupath2  23552  nmoub3i  24124  ubthlem1  24222  ubthlem2  24223  nmopub2tALT  25264  nmfnleub2  25281  lnconi  25388  leoptr  25492  pjnmopi  25503  cdj3lem2b  25792  eulerpartlemb  26703  ltflcei  28372  lxflflp1  28374  itg2addnclem2  28397  itg2addnclem3  28398  itg2addnc  28399  bddiblnc  28415  dvasin  28433  incsequz  28597  mettrifi  28606  equivbnd  28642  bfplem1  28674  jm2.17b  29257  fmul01lt1lem2  29719  eluzge0nn0  30142  uzuzle  30143  elfz2z  30151  wwlksubclwwlk  30419  difelfznle  30441  clwlkfclwwlk  30470
  Copyright terms: Public domain W3C validator