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

Theorem lelttrd 9738
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 9673 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1227 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 679 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1802   class class class wbr 4433   RRcr 9489    < clt 9626    <_ cle 9627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-resscn 9547  ax-pre-lttri 9564  ax-pre-lttrn 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632
This theorem is referenced by:  lt2msq1  10429  suprzcl  10943  ge0p1rp  11252  elfzolt3  11812  flflp1  11918  ltdifltdiv  11940  modsubdir  12029  seqf1olem1  12120  seqf1olem2  12121  expmulnbnd  12272  discr1  12276  faclbnd5  12350  bcp1nk  12369  hashfun  12469  swrds2  12857  abslt  13121  abs3lem  13145  fzomaxdiflem  13149  reccn2  13393  o1rlimmul  13415  caucvgrlem  13469  geomulcvg  13659  mertenslem1  13667  ef01bndlem  13791  sin01bnd  13792  cos01bnd  13793  sinltx  13796  eirrlem  13809  rpnnen2lem11  13830  ruclem10  13844  bitsfzolem  13956  bitsfzo  13957  bitsinv1lem  13963  smueqlem  14012  pcfaclem  14289  pockthg  14296  prmreclem5  14310  1arith  14317  4sqlem11  14345  4sqlem12  14346  4sqlem13  14347  coe1tmmul2  18185  ssblex  20797  nlmvscnlem2  21060  nlmvscnlem1  21061  nrginvrcnlem  21065  blcvx  21169  icccmplem2  21194  reconnlem2  21198  metdcnlem  21207  icopnfcnv  21308  nmoleub2lem3  21464  ipcnlem2  21550  ipcnlem1  21551  minveclem3b  21709  minveclem3  21710  pjthlem1  21718  pmltpclem2  21727  ivthlem2  21730  ovollb2lem  21765  iundisj  21824  uniioombllem3  21860  opnmbllem  21876  itg2monolem3  22025  itg2cnlem2  22035  dveflem  22246  dvferm2lem  22253  lhop1lem  22280  dvcnvre  22286  ftc1a  22304  ftc1lem4  22306  coeeulem  22487  dgradd2  22530  aaliou2b  22602  ulmdvlem1  22660  itgulm  22668  radcnvlem1  22673  radcnvlt1  22678  radcnvle  22680  psercnlem1  22685  pserdvlem1  22687  pserdv  22689  abelthlem2  22692  abelthlem7  22698  cosordlem  22783  tanord1  22789  efif1olem1  22794  logcnlem3  22890  logcnlem4  22891  efopnlem1  22902  logtayl  22906  cxpcn3lem  22986  birthdaylem3  23148  efrlim  23164  ftalem1  23211  ftalem2  23212  ftalem5  23215  basellem1  23219  basellem3  23221  perfectlem2  23370  bposlem1  23424  bposlem3  23426  bposlem6  23429  lgsdirprm  23469  lgsqrlem2  23482  lgseisen  23493  lgsquadlem1  23494  lgsquadlem2  23495  2sqlem8  23512  2sqblem  23517  dchrvmasumiflem1  23551  pntrmax  23614  pntlemc  23645  pntlemg  23648  pntlemr  23652  axpaschlem  24108  axlowdimlem16  24125  clwwisshclwwlem  24671  eupap1  24841  smcnlem  25472  minvecolem3  25657  pjhthlem1  26174  nmcexi  26810  iundisjf  27313  iundisjfi  27466  dya2icoseg  28114  lgamgulmlem2  28438  lgamucov  28446  subfaclim  28498  bpoly4  29789  opnmbllem0  30018  mblfinlem3  30021  mblfinlem4  30022  ftc1cnnclem  30056  ftc1anclem7  30064  isbnd3  30248  cntotbnd  30260  rrnequiv  30299  icodiamlt  30724  irrapxlem1  30726  pell14qrgapw  30780  monotoddzzfi  30846  ltrmynn0  30854  jm2.24nn  30865  acongeq  30889  jm2.26lem3  30911  jm3.1lem2  30928  rfcnnnub  31358  zltlesub  31413  monoords  31441  fmul01lt1lem1  31502  fmul01lt1lem2  31503  lptre2pt  31550  addlimc  31558  0ellimcdiv  31559  limclner  31561  icccncfext  31593  ioodvbdlimc1lem1  31628  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  iblspltprt  31658  itgspltprt  31664  stoweidlem5  31672  stoweidlem11  31678  stoweidlem13  31680  stoweidlem14  31681  stoweidlem25  31692  stoweidlem26  31693  stoweidlem42  31709  stoweidlem59  31726  stoweid  31730  wallispilem3  31734  wallispilem4  31735  wallispilem5  31736  fourierdlem10  31784  fourierdlem11  31785  fourierdlem12  31786  fourierdlem15  31789  fourierdlem20  31794  fourierdlem24  31798  fourierdlem30  31804  fourierdlem31  31805  fourierdlem33  31807  fourierdlem40  31814  fourierdlem41  31815  fourierdlem42  31816  fourierdlem43  31817  fourierdlem44  31818  fourierdlem46  31820  fourierdlem47  31821  fourierdlem48  31822  fourierdlem50  31824  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem76  31850  fourierdlem77  31851  fourierdlem78  31852  fourierdlem79  31853  fourierdlem87  31861  fourierdlem91  31865  fourierdlem92  31866  fourierdlem103  31877  fourierdlem104  31878  fouriersw  31899  pgrple2abl  32666  isosctrlem1ALT  33442
  Copyright terms: Public domain W3C validator