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

Theorem lelttrd 9516
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 9452 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1211 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 672 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   class class class wbr 4280   RRcr 9268    < clt 9405    <_ cle 9406
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 9326  ax-pre-lttri 9343  ax-pre-lttrn 9344
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 9407  df-mnf 9408  df-xr 9409  df-ltxr 9410  df-le 9411
This theorem is referenced by:  lt2msq1  10202  suprzcl  10708  ge0p1rp  11006  elfzolt3  11545  ltdifltdiv  11661  modsubdir  11750  seqf1olem1  11828  seqf1olem2  11829  expmulnbnd  11979  discr1  11983  faclbnd5  12057  bcp1nk  12076  hashfun  12182  swrds2  12528  abslt  12785  abs3lem  12809  fzomaxdiflem  12813  reccn2  13057  o1rlimmul  13079  caucvgrlem  13133  geomulcvg  13318  mertenslem1  13326  ef01bndlem  13450  sin01bnd  13451  cos01bnd  13452  sinltx  13455  eirrlem  13468  rpnnen2lem11  13489  ruclem10  13503  bitsfzolem  13612  bitsfzo  13613  bitsinv1lem  13619  smueqlem  13668  pcfaclem  13942  pockthg  13949  prmreclem5  13963  1arith  13970  4sqlem11  13998  4sqlem12  13999  4sqlem13  14000  coe1tmmul2  17626  ssblex  19844  nlmvscnlem2  20107  nlmvscnlem1  20108  nrginvrcnlem  20112  blcvx  20216  icccmplem2  20241  reconnlem2  20245  metdcnlem  20254  icopnfcnv  20355  nmoleub2lem3  20511  ipcnlem2  20597  ipcnlem1  20598  minveclem3b  20756  minveclem3  20757  pjthlem1  20765  pmltpclem2  20774  ivthlem2  20777  ovollb2lem  20812  iundisj  20870  uniioombllem3  20906  opnmbllem  20922  itg2monolem3  21071  itg2cnlem2  21081  dveflem  21292  dvferm2lem  21299  lhop1lem  21326  dvcnvre  21332  ftc1a  21350  ftc1lem4  21352  coeeulem  21576  dgradd2  21619  aaliou2b  21691  ulmdvlem1  21749  itgulm  21757  radcnvlem1  21762  radcnvlt1  21767  radcnvle  21769  psercnlem1  21774  pserdvlem1  21776  pserdv  21778  abelthlem2  21781  abelthlem7  21787  cosordlem  21871  tanord1  21877  efif1olem1  21882  logcnlem3  21973  logcnlem4  21974  efopnlem1  21985  logtayl  21989  cxpcn3lem  22069  birthdaylem3  22231  efrlim  22247  ftalem1  22294  ftalem2  22295  ftalem5  22298  basellem1  22302  basellem3  22304  perfectlem2  22453  bposlem1  22507  bposlem3  22509  bposlem6  22512  lgsdirprm  22552  lgsqrlem2  22565  lgseisen  22576  lgsquadlem1  22577  lgsquadlem2  22578  2sqlem8  22595  2sqblem  22600  dchrvmasumiflem1  22634  pntrmax  22697  pntlemc  22728  pntlemg  22731  pntlemr  22735  axpaschlem  23008  axlowdimlem16  23025  eupap1  23419  smcnlem  23914  minvecolem3  24099  pjhthlem1  24616  nmcexi  25252  iundisjf  25754  iundisjfi  25902  dya2icoseg  26545  lgamgulmlem2  26863  lgamucov  26871  subfaclim  26923  bpoly4  28048  lxflflp1  28262  opnmbllem0  28268  mblfinlem3  28271  mblfinlem4  28272  ftc1cnnclem  28306  ftc1anclem7  28314  isbnd3  28524  cntotbnd  28536  rrnequiv  28575  icodiamlt  29003  irrapxlem1  29005  pell14qrgapw  29059  monotoddzzfi  29125  ltrmynn0  29133  jm2.24nn  29144  acongeq  29168  jm2.26lem3  29192  jm3.1lem2  29209  rfcnnnub  29600  fmul01lt1lem1  29607  fmul01lt1lem2  29608  stoweidlem5  29643  stoweidlem11  29649  stoweidlem13  29651  stoweidlem14  29652  stoweidlem25  29663  stoweidlem26  29664  stoweidlem42  29680  stoweidlem59  29697  stoweid  29701  wallispilem3  29705  wallispilem4  29706  wallispilem5  29707  clwwisshclwwlem  30313  pgrple2abel  30596  isosctrlem1ALT  31369
  Copyright terms: Public domain W3C validator