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

Theorem lelttrd 9729
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 9664 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <_  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1226 . 2  |-  ( ph  ->  ( ( A  <_  B  /\  B  <  C
)  ->  A  <  C ) )
81, 2, 7mp2and 677 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   class class class wbr 4439   RRcr 9480    < clt 9617    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-pre-lttri 9555  ax-pre-lttrn 9556
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623
This theorem is referenced by:  lt2msq1  10423  suprzcl  10938  ge0p1rp  11250  elfzolt3  11814  flflp1  11925  ltdifltdiv  11948  modsubdir  12037  seqf1olem1  12128  seqf1olem2  12129  expmulnbnd  12280  discr1  12284  faclbnd5  12358  bcp1nk  12377  hashfun  12479  swrds2  12874  abslt  13229  abs3lem  13253  fzomaxdiflem  13257  reccn2  13501  o1rlimmul  13523  caucvgrlem  13577  geomulcvg  13767  mertenslem1  13775  ef01bndlem  14001  sin01bnd  14002  cos01bnd  14003  sinltx  14006  eirrlem  14019  rpnnen2lem11  14042  ruclem10  14056  bitsfzolem  14168  bitsfzo  14169  bitsinv1lem  14175  smueqlem  14224  pcfaclem  14501  pockthg  14508  prmreclem5  14522  1arith  14529  4sqlem11  14557  4sqlem12  14558  4sqlem13  14559  coe1tmmul2  18512  ssblex  21097  nlmvscnlem2  21360  nlmvscnlem1  21361  nrginvrcnlem  21365  blcvx  21469  icccmplem2  21494  reconnlem2  21498  metdcnlem  21507  icopnfcnv  21608  nmoleub2lem3  21764  ipcnlem2  21850  ipcnlem1  21851  minveclem3b  22009  minveclem3  22010  pjthlem1  22018  pmltpclem2  22027  ivthlem2  22030  ovollb2lem  22065  iundisj  22124  uniioombllem3  22160  opnmbllem  22176  itg2monolem3  22325  itg2cnlem2  22335  dveflem  22546  dvferm2lem  22553  lhop1lem  22580  dvcnvre  22586  ftc1a  22604  ftc1lem4  22606  coeeulem  22787  dgradd2  22831  aaliou2b  22903  ulmdvlem1  22961  itgulm  22969  radcnvlem1  22974  radcnvlt1  22979  radcnvle  22981  psercnlem1  22986  pserdvlem1  22988  pserdv  22990  abelthlem2  22993  abelthlem7  22999  cosordlem  23084  tanord1  23090  efif1olem1  23095  logcnlem3  23193  logcnlem4  23194  efopnlem1  23205  logtayl  23209  cxpcn3lem  23289  birthdaylem3  23481  efrlim  23497  ftalem1  23544  ftalem2  23545  ftalem5  23548  basellem1  23552  basellem3  23554  perfectlem2  23703  bposlem1  23757  bposlem3  23759  bposlem6  23762  lgsdirprm  23802  lgsqrlem2  23815  lgseisen  23826  lgsquadlem1  23827  lgsquadlem2  23828  2sqlem8  23845  2sqblem  23850  dchrvmasumiflem1  23884  pntrmax  23947  pntlemc  23978  pntlemg  23981  pntlemr  23985  axpaschlem  24445  axlowdimlem16  24462  clwwisshclwwlem  25008  eupap1  25178  smcnlem  25805  minvecolem3  25990  pjhthlem1  26507  nmcexi  27143  iundisjf  27659  iundisjfi  27835  dya2icoseg  28485  lgamgulmlem2  28836  lgamucov  28844  subfaclim  28896  bpoly4  30049  opnmbllem0  30290  mblfinlem3  30293  mblfinlem4  30294  ftc1cnnclem  30328  ftc1anclem7  30336  isbnd3  30520  cntotbnd  30532  rrnequiv  30571  icodiamlt  30995  irrapxlem1  30997  pell14qrgapw  31051  monotoddzzfi  31117  ltrmynn0  31125  jm2.24nn  31136  acongeq  31160  jm2.26lem3  31182  jm3.1lem2  31199  binomcxplemnotnn0  31502  rfcnnnub  31651  zltlesub  31708  monoords  31735  fmul01lt1lem1  31817  fmul01lt1lem2  31818  lptre2pt  31885  addlimc  31893  0ellimcdiv  31894  limclner  31896  icccncfext  31929  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnmul  31979  iblspltprt  32011  itgspltprt  32017  stoweidlem5  32026  stoweidlem11  32032  stoweidlem13  32034  stoweidlem14  32035  stoweidlem25  32046  stoweidlem26  32047  stoweidlem42  32063  stoweidlem59  32080  stoweid  32084  wallispilem3  32088  wallispilem4  32089  wallispilem5  32090  fourierdlem10  32138  fourierdlem11  32139  fourierdlem12  32140  fourierdlem15  32143  fourierdlem20  32148  fourierdlem24  32152  fourierdlem30  32158  fourierdlem31  32159  fourierdlem33  32161  fourierdlem40  32168  fourierdlem41  32169  fourierdlem42  32170  fourierdlem43  32171  fourierdlem44  32172  fourierdlem46  32174  fourierdlem47  32175  fourierdlem48  32176  fourierdlem50  32178  fourierdlem63  32191  fourierdlem64  32192  fourierdlem65  32193  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem77  32205  fourierdlem78  32206  fourierdlem79  32207  fourierdlem87  32215  fourierdlem91  32219  fourierdlem92  32220  fourierdlem103  32231  fourierdlem104  32232  fouriersw  32253  etransclem19  32275  etransclem23  32279  etransclem48  32304  pgrple2abl  33212  logbpw2m1  33442  dignn0ldlem  33477  isosctrlem1ALT  34135
  Copyright terms: Public domain W3C validator