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

Theorem lelttrd 9795
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 9726 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1265 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 684 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1869   class class class wbr 4421   RRcr 9540    < clt 9677    <_ cle 9678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-resscn 9598  ax-pre-lttri 9615  ax-pre-lttrn 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-er 7369  df-en 7576  df-dom 7577  df-sdom 7578  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683
This theorem is referenced by:  lt2msq1  10492  suprzcl  11017  ge0p1rp  11333  elfzolt3  11932  flflp1  12044  ltdifltdiv  12067  modsubdir  12159  seqf1olem1  12253  seqf1olem2  12254  expmulnbnd  12405  discr1  12409  faclbnd5  12484  bcp1nk  12503  hashfun  12608  swrds2  13014  abslt  13371  abs3lem  13395  fzomaxdiflem  13399  reccn2  13653  o1rlimmul  13675  caucvgrlem  13729  caucvgrlemOLD  13730  geomulcvg  13925  mertenslem1  13933  bpoly4  14105  ef01bndlem  14231  sin01bnd  14232  cos01bnd  14233  sinltx  14236  eirrlem  14249  rpnnen2lem11  14270  ruclem10  14284  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsinv1lem  14408  smueqlem  14457  pcfaclem  14836  pockthg  14843  prmreclem5  14857  1arith  14864  4sqlem11  14892  4sqlem12  14893  4sqlem13OLD  14894  4sqlem13  14900  coe1tmmul2  18862  ssblex  21435  nlmvscnlem2  21680  nlmvscnlem1  21681  nrginvrcnlem  21685  blcvx  21808  icccmplem2  21833  reconnlem2  21837  metdcnlem  21846  icopnfcnv  21962  nmoleub2lem3  22121  ipcnlem2  22207  ipcnlem1  22208  minveclem3b  22362  minveclem3  22363  minveclem3bOLD  22374  minveclem3OLD  22375  pjthlem1  22383  pmltpclem2  22392  ivthlem2  22395  ovollb2lem  22433  iundisj  22493  uniioombllem3  22535  opnmbllem  22551  itg2monolem3  22702  itg2cnlem2  22712  dveflem  22923  dvferm2lem  22930  lhop1lem  22957  dvcnvre  22963  ftc1a  22981  ftc1lem4  22983  coeeulem  23170  dgradd2  23214  aaliou2b  23289  ulmdvlem1  23347  itgulm  23355  radcnvlem1  23360  radcnvlt1  23365  radcnvle  23367  psercnlem1  23372  pserdvlem1  23374  pserdv  23376  abelthlem2  23379  abelthlem7  23385  cosordlem  23472  tanord1  23478  efif1olem1  23483  logcnlem3  23581  logcnlem4  23582  efopnlem1  23593  logtayl  23597  cxpcn3lem  23679  birthdaylem3  23871  efrlim  23887  lgamgulmlem2  23947  lgamucov  23955  ftalem1  23989  ftalem2  23990  ftalem5  23993  ftalem5OLD  23995  basellem1  23999  basellem3  24001  perfectlem2  24150  bposlem1  24204  bposlem3  24206  bposlem6  24209  lgsdirprm  24249  lgsqrlem2  24262  lgseisen  24273  lgsquadlem1  24274  lgsquadlem2  24275  2sqlem8  24292  2sqblem  24297  dchrvmasumiflem1  24331  pntrmax  24394  pntlemc  24425  pntlemg  24428  pntlemr  24432  axpaschlem  24962  axlowdimlem16  24979  clwwisshclwwlem  25526  eupap1  25696  smcnlem  26325  minvecolem3  26510  minvecolem3OLD  26520  pjhthlem1  27036  nmcexi  27671  iundisjf  28195  iundisjfi  28372  psgnfzto1stlem  28615  dya2icoseg  29101  subfaclim  29913  bcprod  30375  poimirlem6  31866  poimirlem7  31867  poimirlem12  31872  poimirlem15  31875  poimirlem17  31877  poimirlem19  31879  poimirlem20  31880  poimirlem23  31883  poimirlem24  31884  opnmbllem0  31896  mblfinlem3  31899  mblfinlem4  31900  ftc1cnnclem  31935  ftc1anclem7  31943  isbnd3  32036  cntotbnd  32048  rrnequiv  32087  icodiamlt  35590  irrapxlem1  35592  pell14qrgapw  35648  monotoddzzfi  35716  ltrmynn0  35724  jm2.24nn  35735  acongeq  35759  jm2.26lem3  35782  jm3.1lem2  35799  binomcxplemnotnn0  36569  isosctrlem1ALT  37198  rfcnnnub  37224  zltlesub  37343  monoords  37362  supxrge  37409  fmul01lt1lem1  37488  fmul01lt1lem2  37489  lptre2pt  37546  addlimc  37555  0ellimcdiv  37556  limclner  37558  icccncfext  37591  ioodvbdlimc1lem1  37629  ioodvbdlimc1lem2  37630  ioodvbdlimc1lem1OLD  37631  ioodvbdlimc1lem2OLD  37632  ioodvbdlimc2lem  37634  ioodvbdlimc2lemOLD  37635  dvnmul  37644  iblspltprt  37676  itgspltprt  37682  stoweidlem5  37691  stoweidlem11  37697  stoweidlem13  37699  stoweidlem14  37700  stoweidlem25  37711  stoweidlem26  37712  stoweidlem42  37729  stoweidlem59  37746  stoweid  37751  wallispilem3  37755  wallispilem4  37756  wallispilem5  37757  fourierdlem10  37805  fourierdlem11  37806  fourierdlem12  37807  fourierdlem15  37810  fourierdlem20  37815  fourierdlem24  37819  fourierdlem30  37825  fourierdlem31  37826  fourierdlem31OLD  37827  fourierdlem33  37829  fourierdlem40  37836  fourierdlem41  37837  fourierdlem42  37838  fourierdlem42OLD  37839  fourierdlem43  37840  fourierdlem44  37841  fourierdlem46  37842  fourierdlem47  37843  fourierdlem48  37844  fourierdlem50  37846  fourierdlem63  37859  fourierdlem64  37860  fourierdlem65  37861  fourierdlem73  37869  fourierdlem74  37870  fourierdlem75  37871  fourierdlem76  37872  fourierdlem77  37873  fourierdlem78  37874  fourierdlem79  37875  fourierdlem87  37883  fourierdlem91  37887  fourierdlem92  37888  fourierdlem103  37899  fourierdlem104  37900  fouriersw  37921  etransclem19  37944  etransclem23  37948  etransclem48OLD  37973  etransclem48  37974  iundjiun  38083  omeiunltfirp  38125  caratheodorylem1  38132  hoicvr  38151  iccpartgt  38459  perfectALTVlem2  38562  bgoldbtbndlem2  38619  pgrple2abl  39456  logbpw2m1  39684  dignn0ldlem  39719
  Copyright terms: Public domain W3C validator