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

Theorem lelttrd 9218
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 9155 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1184 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 661 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   class class class wbr 4204   RRcr 8979    < clt 9110    <_ cle 9111
This theorem is referenced by:  lt2msq1  9883  suprzcl  10339  ge0p1rp  10630  elfzolt3  11139  modsubdir  11275  seqf1olem1  11352  seqf1olem2  11353  expmulnbnd  11501  discr1  11505  faclbnd5  11579  bcp1nk  11598  hashfun  11690  swrds2  11870  abslt  12108  abs3lem  12132  fzomaxdiflem  12136  reccn2  12380  o1rlimmul  12402  caucvgrlem  12456  geomulcvg  12643  mertenslem1  12651  ef01bndlem  12775  sin01bnd  12776  cos01bnd  12777  sinltx  12780  eirrlem  12793  rpnnen2lem11  12814  ruclem10  12828  bitsfzolem  12936  bitsfzo  12937  bitsinv1lem  12943  smueqlem  12992  pcfaclem  13257  pockthg  13264  prmreclem5  13278  1arith  13285  4sqlem11  13313  4sqlem12  13314  4sqlem13  13315  coe1tmmul2  16658  ssblex  18448  nlmvscnlem2  18711  nlmvscnlem1  18712  nrginvrcnlem  18716  blcvx  18819  icccmplem2  18844  reconnlem2  18848  metdcnlem  18857  icopnfcnv  18957  nmoleub2lem3  19113  ipcnlem2  19188  ipcnlem1  19189  minveclem3b  19319  minveclem3  19320  pjthlem1  19328  pmltpclem2  19336  ivthlem2  19339  ovollb2lem  19374  iundisj  19432  uniioombllem3  19467  opnmbllem  19483  itg2monolem3  19634  itg2cnlem2  19644  dveflem  19853  dvferm2lem  19860  lhop1lem  19887  dvcnvre  19893  ftc1a  19911  ftc1lem4  19913  coeeulem  20133  dgradd2  20176  aaliou2b  20248  ulmdvlem1  20306  itgulm  20314  radcnvlem1  20319  radcnvlt1  20324  radcnvle  20326  psercnlem1  20331  pserdvlem1  20333  pserdv  20335  abelthlem2  20338  abelthlem7  20344  cosordlem  20423  tanord1  20429  efif1olem1  20434  logcnlem3  20525  logcnlem4  20526  efopnlem1  20537  logtayl  20541  cxpcn3lem  20621  birthdaylem3  20782  efrlim  20798  ftalem1  20845  ftalem2  20846  ftalem5  20849  basellem1  20853  basellem3  20855  perfectlem2  21004  bposlem1  21058  bposlem3  21060  bposlem6  21063  lgsdirprm  21103  lgsqrlem2  21116  lgseisen  21127  lgsquadlem1  21128  lgsquadlem2  21129  2sqlem8  21146  2sqblem  21151  dchrvmasumiflem1  21185  pntrmax  21248  pntlemc  21279  pntlemg  21282  pntlemr  21286  eupap1  21688  smcnlem  22183  minvecolem3  22368  pjhthlem1  22883  nmcexi  23519  iundisjf  24019  iundisjfi  24142  dya2icoseg  24617  lgamgulmlem2  24804  lgamucov  24812  subfaclim  24864  axpaschlem  25844  axlowdimlem16  25861  bpoly4  26070  lxflflp1  26206  mblfinlem  26207  mblfinlem2  26208  mblfinlem3  26209  ftc1cnnclem  26241  isbnd3  26447  cntotbnd  26459  rrnequiv  26498  icodiamlt  26837  irrapxlem1  26839  pell14qrgapw  26893  monotoddzzfi  26959  ltrmynn0  26967  jm2.24nn  26978  acongeq  27002  jm2.26lem3  27026  jm3.1lem2  27043  rfcnnnub  27638  fmul01lt1lem1  27645  fmul01lt1lem2  27646  stoweidlem5  27685  stoweidlem11  27691  stoweidlem13  27693  stoweidlem14  27694  stoweidlem25  27705  stoweidlem26  27706  stoweidlem42  27722  stoweidlem59  27739  stoweid  27743  wallispilem3  27747  wallispilem4  27748  wallispilem5  27749  ltdifltdiv  28090  isosctrlem1ALT  28947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-resscn 9037  ax-pre-lttri 9054  ax-pre-lttrn 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116
  Copyright terms: Public domain W3C validator