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

Theorem lelttrd 8990
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 8928 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1182 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 660 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   class class class wbr 4039   RRcr 8752    < clt 8883    <_ cle 8884
This theorem is referenced by:  lt2msq1  9655  suprzcl  10107  ge0p1rp  10398  elfzolt3  10900  modsubdir  11024  seqf1olem1  11101  seqf1olem2  11102  expmulnbnd  11249  discr1  11253  faclbnd5  11327  bcp1nk  11345  hashfun  11405  swrds2  11576  abslt  11814  abs3lem  11838  fzomaxdiflem  11842  reccn2  12086  o1rlimmul  12108  caucvgrlem  12161  geomulcvg  12348  mertenslem1  12356  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  sinltx  12485  eirrlem  12498  rpnnen2lem11  12519  ruclem10  12533  bitsfzolem  12641  bitsfzo  12642  bitsinv1lem  12648  smueqlem  12697  pcfaclem  12962  pockthg  12969  prmreclem5  12983  1arith  12990  4sqlem11  13018  4sqlem12  13019  4sqlem13  13020  coe1tmmul2  16368  ssblex  17990  nlmvscnlem2  18212  nlmvscnlem1  18213  nrginvrcnlem  18217  blcvx  18320  icccmplem2  18344  reconnlem2  18348  metdcnlem  18357  icopnfcnv  18456  nmoleub2lem3  18612  ipcnlem2  18687  ipcnlem1  18688  minveclem3b  18808  minveclem3  18809  pjthlem1  18817  pmltpclem2  18825  ivthlem2  18828  ovollb2lem  18863  iundisj  18921  uniioombllem3  18956  opnmbllem  18972  itg2monolem3  19123  itg2cnlem2  19133  dveflem  19342  dvferm2lem  19349  lhop1lem  19376  dvcnvre  19382  ftc1a  19400  ftc1lem4  19402  coeeulem  19622  dgradd2  19665  aaliou2b  19737  ulmdvlem1  19793  itgulm  19800  radcnvlem1  19805  radcnvlt1  19810  radcnvle  19812  psercnlem1  19817  pserdvlem1  19819  pserdv  19821  abelthlem2  19824  abelthlem7  19830  cosordlem  19909  tanord1  19915  efif1olem1  19920  logcnlem3  20007  logcnlem4  20008  efopnlem1  20019  logtayl  20023  cxpcn3lem  20103  birthdaylem3  20264  efrlim  20280  ftalem1  20326  ftalem2  20327  ftalem5  20330  basellem1  20334  basellem3  20336  perfectlem2  20485  bposlem1  20539  bposlem3  20541  bposlem6  20544  lgsdirprm  20584  lgsqrlem2  20597  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  2sqlem8  20627  2sqblem  20632  dchrvmasumiflem1  20666  pntrmax  20729  pntlemc  20760  pntlemg  20763  pntlemr  20767  smcnlem  21286  minvecolem3  21471  pjhthlem1  21986  nmcexi  22622  sqsscirc1  23307  iundisjfi  23378  iundisjf  23380  dya2iocseg  23594  subfaclim  23734  eupap1  23915  axpaschlem  24640  axlowdimlem16  24657  bpoly4  24866  lxflflp1  25000  ftc1cnnclem  25024  isbnd3  26611  cntotbnd  26623  rrnequiv  26662  icodiamlt  27008  irrapxlem1  27010  pell14qrgapw  27064  monotoddzzfi  27130  ltrmynn0  27138  jm2.24nn  27149  acongeq  27173  jm2.26lem3  27197  jm3.1lem2  27214  stoweidlem13  27865
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-resscn 8810  ax-pre-lttri 8827  ax-pre-lttrn 8828
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889
  Copyright terms: Public domain W3C validator