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

Theorem letr 9456
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 9449 . . . . 5  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C )
) )
213adant1 999 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( B  <_  C  <->  ( B  <  C  \/  B  =  C ) ) )
32adantr 462 . . 3  |-  ( ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  /\  A  <_  B )  ->  ( B  <_  C 
<->  ( B  <  C  \/  B  =  C
) ) )
4 lelttr 9453 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
5 ltle 9451 . . . . . . 7  |-  ( ( A  e.  RR  /\  C  e.  RR )  ->  ( A  <  C  ->  A  <_  C )
)
653adant2 1000 . . . . . 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 4284 . . . . . 6  |-  ( B  =  C  ->  ( A  <_  B  <->  A  <_  C ) )
109biimpcd 224 . . . . 5  |-  ( A  <_  B  ->  ( B  =  C  ->  A  <_  C ) )
1110adantl 463 . . . 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 598 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 958    = wceq 1362    e. wcel 1755   class class class wbr 4280   RRcr 9269    < clt 9406    <_ cle 9407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-pre-lttri 9344  ax-pre-lttrn 9345
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412
This theorem is referenced by:  letri  9491  letrd  9516  le2add  9809  le2sub  9826  p1le  10160  lemul12b  10174  lemul12a  10175  zletr  10677  peano2uz2  10717  uzletr  10857  uztrn  10865  uzss  10869  elfz0fzfz0  11472  fz0fzelfz0  11473  fz0fzdiffz0  11476  elfzmlbm  11477  elfzmlbp  11478  elfz1b  11511  ssfzoulel  11605  ssfzo12bi  11606  flge  11639  monoord  11820  leexp2r  11905  expubnd  11908  le2sq2  11925  facwordi  12049  faclbnd3  12052  facavg  12061  brfi1uzind  12203  swrdswrdlem  12337  swrdccat  12368  sqrlem1  12716  sqrlem6  12721  sqrlem7  12722  leabs  12772  limsupbnd2  12945  rlim3  12960  lo1bdd2  12986  lo1bddrp  12987  o1lo1  12999  lo1mul  13089  lo1le  13113  isercolllem2  13127  iseraltlem2  13144  fsumabs  13247  cvgrat  13326  ruclem9  13503  algcvga  13737  prmfac1  13787  eulerthlem2  13840  modprm0  13856  prmreclem1  13960  prmreclem4  13963  4sqlem11  13999  vdwnnlem3  14041  gsumbagdiaglem  17379  zntoslem  17831  cnllycmp  20370  evth  20373  ovoliunlem2  20828  ovolicc2lem3  20844  itg2monolem1  21070  coeaddlem  21601  coemullem  21602  aalioulem5  21687  aalioulem6  21688  sincosq1lem  21844  emcllem6  22279  ftalem3  22297  fsumvma2  22438  chpchtsum  22443  bcmono  22501  bposlem5  22512  lgsquadlem1  22578  dchrisum0lem1  22650  pntrsumbnd2  22701  pntleml  22745  brbtwn2  22974  axlowdimlem17  23027  axlowdim  23030  eupath2  23424  nmoub3i  23996  ubthlem1  24094  ubthlem2  24095  nmopub2tALT  25136  nmfnleub2  25153  lnconi  25260  leoptr  25364  pjnmopi  25375  cdj3lem2b  25664  eulerpartlemb  26599  ltflcei  28263  lxflflp1  28265  itg2addnclem2  28288  itg2addnclem3  28289  itg2addnc  28290  bddiblnc  28306  dvasin  28324  incsequz  28488  mettrifi  28497  equivbnd  28533  bfplem1  28565  jm2.17b  29149  fmul01lt1lem2  29611  eluzge0nn0  30035  uzuzle  30036  elfz2z  30044  wwlksubclwwlk  30312  difelfznle  30334  clwlkfclwwlk  30363
  Copyright terms: Public domain W3C validator