Theorem lttrd 9798

Description: Transitive law deduction for 'less than'. (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 )
lttrd.4	|- ( ph -> A < B )
lttrd.5	|- ( ph -> B < C )

Assertion

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

Proof of Theorem lttrd

Step	Hyp	Ref	Expression
1		lttrd.4	. 2 |- ( ph -> A < B )
2		lttrd.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		lttr 9712	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
7	3, 4, 5, 6	syl3anc 1265	. 2 |- ( ph -> ( ( A < B /\ B < C ) -> A < C ) )
8	1, 2, 7	mp2and 684	1 |- ( ph -> A < C )

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1869   class class class wbr 4421   RRcr 9540   < clt 9677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-resscn 9598  ax-pre-lttrn 9616

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-er 7369  df-en 7576  df-dom 7577  df-sdom 7578  df-pnf 9679  df-mnf 9680  df-ltxr 9682

This theorem is referenced by:  expgt1  12311  ltexp2a  12325  expcan  12326  ltexp2  12327  leexp2  12328  expnlbnd2  12404  expmulnbnd  12405  reccn2  13653  efgt1  14163  tanhlt1  14207  ruclem2  14277  pythagtriplem13  14770  fldivp1  14835  4sqlem12  14893  sylow1lem1  17243  telgsums  17616  chfacffsupp  19872  chfacfscmul0  19874  chfacfpmmul0  19878  nrginvrcnlem  21685  iccntr  21831  icccmplem2  21833  opnreen  21841  pjthlem1  22383  pmltpclem2  22392  ovollb2lem  22433  opnmbllem  22551  volivth  22557  lhop1lem  22957  dvcnvrelem1  22961  dvcvx  22964  ftc1lem4  22983  aaliou3lem7  23297  ulmdvlem1  23347  reeff1olem  23393  pilem2  23399  pilem2OLD  23400  pilem3  23401  pilem3OLD  23402  tangtx  23452  tanord1  23478  tanord  23479  rplogcl  23545  logimul  23555  logcnlem3  23581  efopnlem1  23593  cxplt  23631  cxple  23632  cxpcn3lem  23679  asinsin  23810  atanlogaddlem  23831  atanlogsublem  23833  cxp2limlem  23893  cxp2lim  23894  zetacvg  23932  lgamucov  23955  lgamcvg2  23972  ftalem1  23989  mersenne  24147  bposlem2  24205  bposlem6  24209  bposlem9  24212  lgsqrlem2  24262  lgsquadlem2  24275  chebbnd1lem2  24300  chebbnd1lem3  24301  chebbnd1  24302  chtppilimlem1  24303  chto1ub  24306  mulog2sumlem2  24365  chpdifbndlem1  24383  selberg3lem1  24387  pntrlog2bndlem2  24408  pntrlog2bndlem4  24410  pntpbnd1a  24415  pntpbnd1  24416  pntpbnd2  24417  pntibndlem1  24419  pntibndlem2  24421  pntibndlem3  24422  pntibnd  24423  pntlemb  24427  pntlemr  24432  pntlemf  24435  pnt  24444  ostth2lem1  24448  ostth2lem3  24465  ostth2lem4  24466  wwlkext2clwwlk  25523  eupap1  25696  frgraogt3nreg  25840  friendshipgt3  25841  pjhthlem1  27036  psgnfzto1stlem  28615  1smat1  28632  sqsscirc1  28716  xrge0iifiso  28743  sgnsub  29417  signslema  29453  poimirlem6  31904  poimirlem7  31905  poimirlem8  31906  poimirlem15  31913  poimirlem20  31918  poimirlem28  31926  opnmbllem0  31934  itg2gt0cn  31955  ftc1cnnclem  31973  ftc1anc  31983  cntotbnd  32086  pellexlem5  35641  pellfundex  35698  pellfundrp  35700  rmspecfund  35721  monotuz  35753  jm3.1lem2  35837  jm3.1lem3  35838  imo72b2  36521  prmunb2  36561  isprm7  36562  neglt  37380  ltadd12dd  37452  lptre2pt  37584  0ellimcdiv  37594  ioodvbdlimc1lem1  37667  ioodvbdlimc1lem1OLD  37669  iblspltprt  37714  itgspltprt  37720  stoweidlem7  37731  stoweidlem11  37735  stoweidlem13  37737  stoweidlem14  37738  stoweidlem26  37750  stoweidlem42  37767  stoweidlem52  37777  stoweidlem59  37784  stoweidlem60  37785  stoweidlem62  37787  stoweidlem62OLD  37788  wallispilem4  37794  wallispi  37796  stirlinglem1  37800  stirlinglem3  37802  stirlinglem6  37805  stirlinglem7  37806  stirlinglem10  37809  stirlinglem11  37810  dirkercncflem1  37829  dirkercncflem2  37830  fourierdlem10  37843  fourierdlem11  37844  fourierdlem12  37845  fourierdlem42  37876  fourierdlem42OLD  37877  fourierdlem47  37881  fourierdlem50  37884  fourierdlem51  37885  fourierdlem73  37907  fourierdlem79  37913  fourierdlem83  37917  fourierdlem103  37937  fourierdlem104  37938  sqwvfoura  37956  sqwvfourb  37957  fouriersw  37959