Theorem ltletrd 10197

Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	|- ( ph -> A e. RR )
ltd.2	|- ( ph -> B e. RR )
letrd.3	|- ( ph -> C e. RR )
ltletrd.4	|- ( ph -> A < B )
ltletrd.5	|- ( ph -> B <_ C )

Assertion

Ref	Expression
ltletrd	|- ( ph -> A < C )

Proof of Theorem ltletrd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 |- ( ph -> A < B )
2		ltletrd.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		ltletr 10129	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
7	3, 4, 5, 6	syl3anc 1326	. 2 |- ( ph -> ( ( A < B /\ B <_ C ) -> A < C ) )
8	1, 2, 7	mp2and 715	1 |- ( ph -> A < C )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  lelttrdi  10199  uzwo3  11783  rpgecl  11859  fznatpl1  12395  modabs  12703  seqf1olem1  12840  expgt1  12898  leexp2a  12916  bernneq3  12992  expnbnd  12993  expmulnbnd  12996  digit1  12998  discr1  13000  hashfun  13224  seqcoll2  13249  abssubne0  14056  icodiamlt  14174  reccn2  14327  isercolllem1  14395  isumltss  14580  fprodntriv  14672  efcllem  14808  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  eirrlem  14932  rpnnen2lem11  14953  ruclem10  14968  bitsmod  15158  bitsinv1lem  15163  smuval2  15204  prmreclem5  15624  1arith  15631  2expltfac  15799  mndodconglem  17960  sylow1lem1  18013  gzrngunit  19812  nlmvscnlem1  22490  nrginvrcnlem  22495  iccpnfhmeo  22744  cnheibor  22754  evth  22758  lebnumlem1  22760  ipcnlem1  23044  lmnn  23061  ovolicc2lem2  23286  itg2monolem1  23517  itg2monolem3  23519  dvferm1lem  23747  dvcnvre  23782  dvfsumlem3  23791  dvfsumrlim  23794  plyco0  23948  aaliou2b  24096  pilem2  24206  cosordlem  24277  logdivlti  24366  logdivle  24368  logcnlem3  24390  logcnlem4  24391  cxpcn3lem  24488  atanre  24612  atanlogaddlem  24640  atans2  24658  ressatans  24661  birthdaylem3  24680  cxp2lim  24703  cxploglim2  24705  jensenlem2  24714  harmonicubnd  24736  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamucov  24764  ftalem2  24800  ftalem5  24803  vma1  24892  chtrpcl  24901  ppiltx  24903  fsumfldivdiaglem  24915  chtub  24937  fsumvma2  24939  chpval2  24943  chpchtsum  24944  chpub  24945  bpos1  25008  bposlem1  25009  bposlem2  25010  bposlem6  25014  gausslemma2dlem0c  25083  lgsquadlem1  25105  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chto1ub  25165  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  rplogsumlem2  25174  dchrisumlema  25177  dchrisumlem3  25180  dchrmusumlema  25182  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0lema  25203  mulog2sumlem1  25223  chpdifbndlem1  25242  chpdifbnd  25244  pntrsumo1  25254  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntlemb  25286  pntlemh  25288  pntlemr  25291  pntlem3  25298  pnt2  25302  ostth2lem1  25307  ostth2lem3  25324  ostth2lem4  25325  axsegconlem7  25803  axsegconlem10  25806  axlowdimlem16  25837  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  clwlkclwwlklem2a2  26894  clwwlksext2edg  26923  smatrcl  29862  1smat1  29870  lmdvg  29999  dya2icoseg  30339  eulerpartlems  30422  reprlt  30697  reprinfz1  30700  breprexplemc  30710  hgt750lemd  30726  hgt750lem  30729  hgt750leme  30736  tgoldbachgtde  30738  subfacval3  31171  knoppndvlem1  32503  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem14  32516  knoppndvlem18  32520  poimirlem7  33416  poimirlem24  33433  poimirlem29  33438  mblfinlem2  33447  itg2addnclem  33461  itg2addnclem3  33463  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anc  33493  areacirclem5  33504  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pell14qrgapw  37440  pellqrex  37443  pellfundgt1  37447  pellfundex  37450  ltrmxnn0  37516  jm2.24nn  37526  jm2.17c  37529  jm2.24  37530  jm2.23  37563  jm3.1lem1  37584  jm3.1lem2  37585  radcnvrat  38513  dstregt0  39493  monoords  39511  uzubioo  39794  fsumnncl  39803  mullimc  39848  mullimcf  39855  sumnnodd  39862  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limclner  39883  limsupgtlem  40009  dvdivbd  40138  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  iblspltprt  40189  itgspltprt  40195  stoweidlem11  40228  stoweidlem24  40241  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem36  40253  stoweidlem42  40259  stoweidlem44  40261  stoweidlem51  40268  stoweidlem59  40276  wallispi  40287  wallispi2lem1  40288  wallispi2  40290  stirlinglem11  40301  dirkertrigeqlem1  40315  dirkeritg  40319  fourierdlem10  40334  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem19  40343  fourierdlem20  40344  fourierdlem30  40354  fourierdlem32  40356  fourierdlem40  40364  fourierdlem41  40365  fourierdlem44  40368  fourierdlem46  40369  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem89  40412  fourierdlem92  40415  fourierdlem103  40426  fourierdlem104  40427  fouriersw  40448  etransclem4  40455  etransclem23  40474  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem48  40499  ioorrnopnlem  40524  sge0uzfsumgt  40661  sge0seq  40663  iundjiun  40677  carageniuncllem2  40736  hoidmvlelem3  40811  iunhoiioolem  40889  vonioolem1  40894  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  bgoldbtbndlem2  41694  logbpw2m1  42361