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

Theorem lelttrd 9162
Description: Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
letrd.3  |-  ( ph  ->  C  e.  RR )
lelttrd.4  |-  ( ph  ->  A  <_  B )
lelttrd.5  |-  ( ph  ->  B  <  C )
Assertion
Ref Expression
lelttrd  |-  ( ph  ->  A  <  C )

Proof of Theorem lelttrd
StepHypRef Expression
1 lelttrd.4 . 2  |-  ( ph  ->  A  <_  B )
2 lelttrd.5 . 2  |-  ( ph  ->  B  <  C )
3 ltd.1 . . 3  |-  ( ph  ->  A  e.  RR )
4 ltd.2 . . 3  |-  ( ph  ->  B  e.  RR )
5 letrd.3 . . 3  |-  ( ph  ->  C  e.  RR )
6 lelttr 9100 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1184 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 661 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717   class class class wbr 4155   RRcr 8924    < clt 9055    <_ cle 9056
This theorem is referenced by:  lt2msq1  9827  suprzcl  10283  ge0p1rp  10574  elfzolt3  11081  modsubdir  11214  seqf1olem1  11291  seqf1olem2  11292  expmulnbnd  11440  discr1  11444  faclbnd5  11518  bcp1nk  11537  hashfun  11629  swrds2  11809  abslt  12047  abs3lem  12071  fzomaxdiflem  12075  reccn2  12319  o1rlimmul  12341  caucvgrlem  12395  geomulcvg  12582  mertenslem1  12590  ef01bndlem  12714  sin01bnd  12715  cos01bnd  12716  sinltx  12719  eirrlem  12732  rpnnen2lem11  12753  ruclem10  12767  bitsfzolem  12875  bitsfzo  12876  bitsinv1lem  12882  smueqlem  12931  pcfaclem  13196  pockthg  13203  prmreclem5  13217  1arith  13224  4sqlem11  13252  4sqlem12  13253  4sqlem13  13254  coe1tmmul2  16597  ssblex  18350  nlmvscnlem2  18594  nlmvscnlem1  18595  nrginvrcnlem  18599  blcvx  18702  icccmplem2  18727  reconnlem2  18731  metdcnlem  18740  icopnfcnv  18840  nmoleub2lem3  18996  ipcnlem2  19071  ipcnlem1  19072  minveclem3b  19198  minveclem3  19199  pjthlem1  19207  pmltpclem2  19215  ivthlem2  19218  ovollb2lem  19253  iundisj  19311  uniioombllem3  19346  opnmbllem  19362  itg2monolem3  19513  itg2cnlem2  19523  dveflem  19732  dvferm2lem  19739  lhop1lem  19766  dvcnvre  19772  ftc1a  19790  ftc1lem4  19792  coeeulem  20012  dgradd2  20055  aaliou2b  20127  ulmdvlem1  20185  itgulm  20193  radcnvlem1  20198  radcnvlt1  20203  radcnvle  20205  psercnlem1  20210  pserdvlem1  20212  pserdv  20214  abelthlem2  20217  abelthlem7  20223  cosordlem  20302  tanord1  20308  efif1olem1  20313  logcnlem3  20404  logcnlem4  20405  efopnlem1  20416  logtayl  20420  cxpcn3lem  20500  birthdaylem3  20661  efrlim  20677  ftalem1  20724  ftalem2  20725  ftalem5  20728  basellem1  20732  basellem3  20734  perfectlem2  20883  bposlem1  20937  bposlem3  20939  bposlem6  20942  lgsdirprm  20982  lgsqrlem2  20995  lgseisen  21006  lgsquadlem1  21007  lgsquadlem2  21008  2sqlem8  21025  2sqblem  21030  dchrvmasumiflem1  21064  pntrmax  21127  pntlemc  21158  pntlemg  21161  pntlemr  21165  eupap1  21548  smcnlem  22043  minvecolem3  22228  pjhthlem1  22743  nmcexi  23379  iundisjf  23874  iundisjfi  23992  dya2icoseg  24423  lgamgulmlem2  24595  lgamucov  24603  subfaclim  24655  axpaschlem  25595  axlowdimlem16  25612  bpoly4  25821  lxflflp1  25954  ftc1cnnclem  25980  isbnd3  26186  cntotbnd  26198  rrnequiv  26237  icodiamlt  26576  irrapxlem1  26578  pell14qrgapw  26632  monotoddzzfi  26698  ltrmynn0  26706  jm2.24nn  26717  acongeq  26741  jm2.26lem3  26765  jm3.1lem2  26782  rfcnnnub  27377  fmul01lt1lem1  27384  fmul01lt1lem2  27385  stoweidlem5  27424  stoweidlem11  27430  stoweidlem13  27432  stoweidlem14  27433  stoweidlem25  27444  stoweidlem26  27445  stoweidlem42  27461  stoweidlem59  27478  stoweid  27482  wallispilem3  27486  wallispilem4  27487  wallispilem5  27488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-resscn 8982  ax-pre-lttri 8999  ax-pre-lttrn 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-er 6843  df-en 7048  df-dom 7049  df-sdom 7050  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061
  Copyright terms: Public domain W3C validator