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

Theorem letr 9589
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 9582 . . . . 5  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C )
) )
213adant1 1012 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C ) ) )
32adantr 463 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  <_  C 
<->  ( B  <  C  \/  B  =  C
) ) )
4 lelttr 9586 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
5 ltle 9584 . . . . . . 7  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A  <  C  ->  A  <_  C )
)
653adant2 1013 . . . . . 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 435 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  < 
C  ->  A  <_  C ) )
9 breq2 4371 . . . . . 6  |-  ( B  =  C  ->  ( A  <_  B  <->  A  <_  C ) )
109biimpcd 224 . . . . 5  |-  ( A  <_  B  ->  ( B  =  C  ->  A  <_  C ) )
1110adantl 464 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  =  C  ->  A  <_  C ) )
128, 11jaod 378 . . 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 601 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 366    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1826   class class class wbr 4367   RRcr 9402    < clt 9539    <_ cle 9540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-resscn 9460  ax-pre-lttri 9477  ax-pre-lttrn 9478
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545
This theorem is referenced by:  letri  9624  letrd  9650  le2add  9952  le2sub  9969  p1le  10302  lemul12b  10316  lemul12a  10317  zletr  10825  peano2uz2  10867  elfz1b  11670  elfz0fzfz0  11701  fz0fzelfz0  11702  fz0fzdiffz0  11705  elfzmlbmOLD  11707  elfzmlbp  11708  difelfznle  11711  elincfzoext  11773  ssfzoulel  11805  ssfzo12bi  11806  flge  11841  flflp1  11843  monoord  12040  leexp2r  12126  expubnd  12129  le2sq2  12146  facwordi  12269  faclbnd3  12272  facavg  12281  brfi1uzind  12436  swrdswrdlem  12595  swrdccat  12629  sqrlem1  13078  sqrlem6  13083  sqrlem7  13084  leabs  13134  limsupbnd2  13308  rlim3  13323  lo1bdd2  13349  lo1bddrp  13350  o1lo1  13362  lo1mul  13452  lo1le  13476  isercolllem2  13490  iseraltlem2  13507  fsumabs  13617  cvgrat  13694  ruclem9  13973  algcvga  14210  prmfac1  14261  eulerthlem2  14314  modprm0  14332  prmreclem1  14436  prmreclem4  14439  4sqlem11  14475  vdwnnlem3  14517  gsumbagdiaglem  18140  zntoslem  18686  cnllycmp  21541  evth  21544  ovoliunlem2  21999  ovolicc2lem3  22015  itg2monolem1  22242  coeaddlem  22731  coemullem  22732  aalioulem5  22817  aalioulem6  22818  sincosq1lem  22975  emcllem6  23447  ftalem3  23465  fsumvma2  23606  chpchtsum  23611  bcmono  23669  bposlem5  23680  lgsquadlem1  23746  dchrisum0lem1  23818  pntrsumbnd2  23869  pntleml  23913  brbtwn2  24329  axlowdimlem17  24382  axlowdim  24385  wwlksubclwwlk  24925  clwlkfclwwlk  24965  eupath2  25101  nmoub3i  25805  ubthlem1  25903  ubthlem2  25904  nmopub2tALT  26944  nmfnleub2  26961  lnconi  27068  leoptr  27172  pjnmopi  27183  cdj3lem2b  27472  eulerpartlemb  28490  ltflcei  30208  itg2addnclem2  30233  itg2addnclem3  30234  itg2addnc  30235  bddiblnc  30251  dvasin  30269  incsequz  30407  mettrifi  30416  equivbnd  30452  bfplem1  30484  jm2.17b  31064  fmul01lt1lem2  31745  eluzge0nn0  32650  elfz2z  32652
  Copyright terms: Public domain W3C validator