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

Theorem lelttrd 9793
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 9724 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1268 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 685 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1887   class class class wbr 4402   RRcr 9538    < clt 9675    <_ cle 9676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-resscn 9596  ax-pre-lttri 9613  ax-pre-lttrn 9614
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681
This theorem is referenced by:  lt2msq1  10490  suprzcl  11015  ge0p1rp  11331  elfzolt3  11930  flflp1  12043  ltdifltdiv  12066  modsubdir  12158  seqf1olem1  12252  seqf1olem2  12253  expmulnbnd  12404  discr1  12408  faclbnd5  12483  bcp1nk  12502  hashfun  12609  swrds2  13020  abslt  13377  abs3lem  13401  fzomaxdiflem  13405  icodiamlt  13497  reccn2  13660  o1rlimmul  13682  caucvgrlem  13736  caucvgrlemOLD  13737  geomulcvg  13932  mertenslem1  13940  bpoly4  14112  ef01bndlem  14238  sin01bnd  14239  cos01bnd  14240  sinltx  14243  eirrlem  14256  rpnnen2lem11  14277  ruclem10  14291  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bitsinv1lem  14415  smueqlem  14464  pcfaclem  14843  pockthg  14850  prmreclem5  14864  1arith  14871  4sqlem11  14899  4sqlem12  14900  4sqlem13OLD  14901  4sqlem13  14907  coe1tmmul2  18869  ssblex  21443  nlmvscnlem2  21688  nlmvscnlem1  21689  nrginvrcnlem  21693  blcvx  21816  icccmplem2  21841  reconnlem2  21845  metdcnlem  21854  icopnfcnv  21970  nmoleub2lem3  22129  ipcnlem2  22215  ipcnlem1  22216  minveclem3b  22370  minveclem3  22371  minveclem3bOLD  22382  minveclem3OLD  22383  pjthlem1  22391  pmltpclem2  22400  ivthlem2  22403  ovollb2lem  22441  iundisj  22501  uniioombllem3  22543  opnmbllem  22559  itg2monolem3  22710  itg2cnlem2  22720  dveflem  22931  dvferm2lem  22938  lhop1lem  22965  dvcnvre  22971  ftc1a  22989  ftc1lem4  22991  coeeulem  23178  dgradd2  23222  aaliou2b  23297  ulmdvlem1  23355  itgulm  23363  radcnvlem1  23368  radcnvlt1  23373  radcnvle  23375  psercnlem1  23380  pserdvlem1  23382  pserdv  23384  abelthlem2  23387  abelthlem7  23393  cosordlem  23480  tanord1  23486  efif1olem1  23491  logcnlem3  23589  logcnlem4  23590  efopnlem1  23601  logtayl  23605  cxpcn3lem  23687  birthdaylem3  23879  efrlim  23895  lgamgulmlem2  23955  lgamucov  23963  ftalem1  23997  ftalem2  23998  ftalem5  24001  ftalem5OLD  24003  basellem1  24007  basellem3  24009  perfectlem2  24158  bposlem1  24212  bposlem3  24214  bposlem6  24217  lgsdirprm  24257  lgsqrlem2  24270  lgseisen  24281  lgsquadlem1  24282  lgsquadlem2  24283  2sqlem8  24300  2sqblem  24305  dchrvmasumiflem1  24339  pntrmax  24402  pntlemc  24433  pntlemg  24436  pntlemr  24440  axpaschlem  24970  axlowdimlem16  24987  clwwisshclwwlem  25534  eupap1  25704  smcnlem  26333  minvecolem3  26518  minvecolem3OLD  26528  pjhthlem1  27044  nmcexi  27679  iundisjf  28199  iundisjfi  28372  psgnfzto1stlem  28613  dya2icoseg  29099  subfaclim  29911  bcprod  30374  poimirlem6  31946  poimirlem7  31947  poimirlem12  31952  poimirlem15  31955  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem23  31963  poimirlem24  31964  opnmbllem0  31976  mblfinlem3  31979  mblfinlem4  31980  ftc1cnnclem  32015  ftc1anclem7  32023  isbnd3  32116  cntotbnd  32128  rrnequiv  32167  irrapxlem1  35666  pell14qrgapw  35722  monotoddzzfi  35790  ltrmynn0  35798  jm2.24nn  35809  acongeq  35833  jm2.26lem3  35856  jm3.1lem2  35873  binomcxplemnotnn0  36705  isosctrlem1ALT  37331  rfcnnnub  37357  zltlesub  37495  monoords  37514  supxrge  37561  fmul01lt1lem1  37662  fmul01lt1lem2  37663  lptre2pt  37720  addlimc  37729  0ellimcdiv  37730  limclner  37732  icccncfext  37765  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem1OLD  37805  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnmul  37818  iblspltprt  37850  itgspltprt  37856  stoweidlem5  37865  stoweidlem11  37871  stoweidlem13  37873  stoweidlem14  37874  stoweidlem25  37885  stoweidlem26  37886  stoweidlem42  37903  stoweidlem59  37920  stoweid  37925  wallispilem3  37929  wallispilem4  37930  wallispilem5  37931  fourierdlem10  37979  fourierdlem11  37980  fourierdlem12  37981  fourierdlem15  37984  fourierdlem20  37989  fourierdlem24  37993  fourierdlem30  37999  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem33  38003  fourierdlem40  38010  fourierdlem41  38011  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem43  38014  fourierdlem44  38015  fourierdlem46  38016  fourierdlem47  38017  fourierdlem48  38018  fourierdlem50  38020  fourierdlem63  38033  fourierdlem64  38034  fourierdlem65  38035  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem77  38047  fourierdlem78  38048  fourierdlem79  38049  fourierdlem87  38057  fourierdlem91  38061  fourierdlem92  38062  fourierdlem103  38073  fourierdlem104  38074  fouriersw  38095  etransclem19  38118  etransclem23  38122  etransclem48OLD  38147  etransclem48  38148  iundjiun  38298  omeiunltfirp  38340  caratheodorylem1  38347  hoicvr  38370  hoidmv1lelem2  38414  hoidmvlelem2  38418  hoiqssbllem2  38445  iccpartgt  38741  perfectALTVlem2  38844  bgoldbtbndlem2  38901  pgrple2abl  40203  logbpw2m1  40431  dignn0ldlem  40466
  Copyright terms: Public domain W3C validator