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

Theorem letr 9726
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 9719 . . . . 5  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C )
) )
213adant1 1023 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C ) ) )
32adantr 466 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  <_  C 
<->  ( B  <  C  \/  B  =  C
) ) )
4 lelttr 9723 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
5 ltle 9721 . . . . . . 7  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A  <  C  ->  A  <_  C )
)
653adant2 1024 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <  C  ->  A  <_  C ) )
74, 6syld 45 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <_  C
) )
87expdimp 438 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  < 
C  ->  A  <_  C ) )
9 breq2 4430 . . . . . 6  |-  ( B  =  C  ->  ( A  <_  B  <->  A  <_  C ) )
109biimpcd 227 . . . . 5  |-  ( A  <_  B  ->  ( B  =  C  ->  A  <_  C ) )
1110adantl 467 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  =  C  ->  A  <_  C ) )
128, 11jaod 381 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( ( B  <  C  \/  B  =  C )  ->  A  <_  C ) )
133, 12sylbid 218 . 2  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  <_  C  ->  A  <_  C
) )
1413expimpd 606 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 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   class class class wbr 4426   RRcr 9537    < clt 9674    <_ cle 9675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-pre-lttri 9612  ax-pre-lttrn 9613
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680
This theorem is referenced by:  letri  9762  letrd  9791  le2add  10095  le2sub  10112  p1le  10447  lemul12b  10461  lemul12a  10462  zletr  10981  peano2uz2  11023  elfz1b  11862  elfz0fzfz0  11893  fz0fzelfz0  11894  fz0fzdiffz0  11897  elfzmlbmOLD  11899  elfzmlbp  11900  difelfznle  11903  elincfzoext  11969  ssfzoulel  12002  ssfzo12bi  12003  flge  12038  flflp1  12040  monoord  12240  leexp2r  12327  expubnd  12330  le2sq2  12347  facwordi  12471  faclbnd3  12474  facavg  12483  brfi1uzind  12641  swrdswrdlem  12800  swrdccat  12834  sqrlem1  13285  sqrlem6  13290  sqrlem7  13291  leabs  13341  limsupbnd2  13524  limsupbnd2OLD  13525  rlim3  13540  lo1bdd2  13566  lo1bddrp  13567  o1lo1  13579  lo1mul  13669  lo1le  13693  isercolllem2  13707  iseraltlem2  13727  fsumabs  13839  cvgrat  13917  ruclem9  14268  algcvga  14509  prmdvdsfz  14611  prmfac1  14633  eulerthlem2  14690  modprm0  14710  prmreclem1  14814  prmreclem4  14817  4sqlem11  14853  vdwnnlem3  14901  gsumbagdiaglem  18525  zntoslem  19049  cnllycmp  21871  evth  21874  ovoliunlem2  22325  ovolicc2lem3  22341  itg2monolem1  22576  coeaddlem  23062  coemullem  23063  aalioulem5  23148  aalioulem6  23149  sincosq1lem  23308  emcllem6  23782  ftalem3  23855  fsumvma2  23996  chpchtsum  24001  bcmono  24059  bposlem5  24070  lgsquadlem1  24136  dchrisum0lem1  24208  pntrsumbnd2  24259  pntleml  24303  brbtwn2  24772  axlowdimlem17  24825  axlowdim  24828  wwlksubclwwlk  25368  clwlkfclwwlk  25408  eupath2  25544  nmoub3i  26250  ubthlem1  26348  ubthlem2  26349  nmopub2tALT  27388  nmfnleub2  27405  lnconi  27512  leoptr  27616  pjnmopi  27627  cdj3lem2b  27916  eulerpartlemb  29018  isbasisrelowllem1  31483  isbasisrelowllem2  31484  ltflcei  31627  itg2addnclem2  31688  itg2addnclem3  31689  itg2addnc  31690  bddiblnc  31706  dvasin  31722  incsequz  31771  mettrifi  31780  equivbnd  31816  bfplem1  31848  jm2.17b  35507  fmul01lt1lem2  37225  iccpartiltu  38116  iccpartgt  38121  eluzge0nn0  38392  elfz2z  38394
  Copyright terms: Public domain W3C validator