Theorem lttrd 9764

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

Hypotheses

Ref	Expression
ltd.1
ltd.2
letrd.3
lttrd.4
lttrd.5

Assertion

Ref	Expression
lttrd

Proof of Theorem lttrd

Step	Hyp	Ref	Expression
1		lttrd.4	. 2
2		lttrd.5	. 2
3		ltd.1	. . 3
4		ltd.2	. . 3
5		letrd.3	. . 3
6		lttr 9682	. . 3
7	3, 4, 5, 6	syl3anc 1228	. 2
8	1, 2, 7	mp2and 679	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   class class class wbr 4452  cr 9512  clt 9649

This theorem is referenced by:  expgt1  12204  ltexp2a  12217  expcan  12218  ltexp2  12219  leexp2  12220  expnlbnd2  12297  expmulnbnd  12298  reccn2  13419  efgt1  13851  tanhlt1  13895  ruclem2  13965  pythagtriplem13  14351  fldivp1  14416  4sqlem12  14474  sylow1lem1  16618  telgsums  17022  chfacffsupp  19357  chfacfscmul0  19359  chfacfpmmul0  19363  nrginvrcnlem  21199  iccntr  21326  icccmplem2  21328  opnreen  21336  pjthlem1  21852  pmltpclem2  21861  ovollb2lem  21899  opnmbllem  22010  volivth  22016  lhop1lem  22414  dvcnvrelem1  22418  dvcvx  22421  ftc1lem4  22440  aaliou3lem7  22745  ulmdvlem1  22795  reeff1olem  22841  pilem2  22847  pilem3  22848  tangtx  22898  tanord1  22924  tanord  22925  rplogcl  22989  logimul  22999  logcnlem3  23025  efopnlem1  23037  cxplt  23075  cxple  23076  cxpcn3lem  23121  asinsin  23223  atanlogaddlem  23244  atanlogsublem  23246  cxp2limlem  23305  cxp2lim  23306  ftalem1  23346  mersenne  23502  bposlem2  23560  bposlem6  23564  bposlem9  23567  lgsqrlem2  23617  lgsquadlem2  23630  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  chto1ub  23661  mulog2sumlem2  23720  chpdifbndlem1  23738  selberg3lem1  23742  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem1  23774  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemb  23782  pntlemr  23787  pntlemf  23790  pnt  23799  ostth2lem1  23803  ostth2lem3  23820  ostth2lem4  23821  wwlkext2clwwlk  24803  eupap1  24976  frgraogt3nreg  25120  friendshipgt3  25121  pjhthlem1  26309  sqsscirc1  27890  xrge0iifiso  27917  sgnsub  28483  signslema  28519  zetacvg  28557  lgamucov  28580  lgamcvg2  28597  opnmbllem0  30050  itg2gt0cn  30070  ftc1cnnclem  30088  ftc1anc  30098  cntotbnd  30292  pellexlem5  30769  pellfundex  30822  pellfundrp  30824  rmspecfund  30845  monotuz  30877  jm3.1lem2  30960  jm3.1lem3  30961  prmunb2  31191  isprm7  31192  neglt  31467  lptre2pt  31646  0ellimcdiv  31655  ioodvbdlimc1lem1  31728  iblspltprt  31772  itgspltprt  31778  stoweidlem7  31789  stoweidlem11  31793  stoweidlem13  31795  stoweidlem14  31796  stoweidlem26  31808  stoweidlem42  31824  stoweidlem52  31834  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  wallispilem4  31850  wallispi  31852  stirlinglem1  31856  stirlinglem3  31858  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  dirkercncflem1  31885  dirkercncflem2  31886  fourierdlem10  31899  fourierdlem11  31900  fourierdlem12  31901  fourierdlem42  31931  fourierdlem47  31936  fourierdlem50  31939  fourierdlem51  31940  fourierdlem73  31962  fourierdlem79  31968  fourierdlem83  31972  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  imo72b2  37993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-pre-lttrn 9588

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-ltxr 9654