Theorem lttrd 9672

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 9590	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
7	3, 4, 5, 6	syl3anc 1226	. 2 |- ( ph -> ( ( A < B /\ B < C ) -> A < C ) )
8	1, 2, 7	mp2and 677	1 |- ( ph -> A < C )

Syntax hints:   -> wi 4   /\ wa 367   e. wcel 1836   class class class wbr 4380   RRcr 9420   < clt 9557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-pre-lttrn 9496

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-ltxr 9562

This theorem is referenced by:  expgt1  12126  ltexp2a  12139  expcan  12140  ltexp2  12141  leexp2  12142  expnlbnd2  12218  expmulnbnd  12219  reccn2  13440  efgt1  13872  tanhlt1  13916  ruclem2  13986  pythagtriplem13  14372  fldivp1  14437  4sqlem12  14495  sylow1lem1  16754  telgsums  17154  chfacffsupp  19461  chfacfscmul0  19463  chfacfpmmul0  19467  nrginvrcnlem  21303  iccntr  21430  icccmplem2  21432  opnreen  21440  pjthlem1  21956  pmltpclem2  21965  ovollb2lem  22003  opnmbllem  22114  volivth  22120  lhop1lem  22518  dvcnvrelem1  22522  dvcvx  22525  ftc1lem4  22544  aaliou3lem7  22849  ulmdvlem1  22899  reeff1olem  22945  pilem2  22951  pilem3  22952  tangtx  23002  tanord1  23028  tanord  23029  rplogcl  23095  logimul  23105  logcnlem3  23131  efopnlem1  23143  cxplt  23181  cxple  23182  cxpcn3lem  23227  asinsin  23358  atanlogaddlem  23379  atanlogsublem  23381  cxp2limlem  23441  cxp2lim  23442  ftalem1  23482  mersenne  23638  bposlem2  23696  bposlem6  23700  bposlem9  23703  lgsqrlem2  23753  lgsquadlem2  23766  chebbnd1lem2  23791  chebbnd1lem3  23792  chebbnd1  23793  chtppilimlem1  23794  chto1ub  23797  mulog2sumlem2  23856  chpdifbndlem1  23874  selberg3lem1  23878  pntrlog2bndlem2  23899  pntrlog2bndlem4  23901  pntpbnd1a  23906  pntpbnd1  23907  pntpbnd2  23908  pntibndlem1  23910  pntibndlem2  23912  pntibndlem3  23913  pntibnd  23914  pntlemb  23918  pntlemr  23923  pntlemf  23926  pnt  23935  ostth2lem1  23939  ostth2lem3  23956  ostth2lem4  23957  wwlkext2clwwlk  24945  eupap1  25118  frgraogt3nreg  25262  friendshipgt3  25263  pjhthlem1  26447  sqsscirc1  28075  xrge0iifiso  28102  sgnsub  28702  signslema  28738  zetacvg  28782  lgamucov  28805  lgamcvg2  28822  opnmbllem0  30251  itg2gt0cn  30272  ftc1cnnclem  30290  ftc1anc  30300  cntotbnd  30494  pellexlem5  30970  pellfundex  31023  pellfundrp  31025  rmspecfund  31046  monotuz  31078  jm3.1lem2  31162  jm3.1lem3  31163  prmunb2  31395  isprm7  31396  neglt  31669  lptre2pt  31847  0ellimcdiv  31856  ioodvbdlimc1lem1  31929  iblspltprt  31973  itgspltprt  31979  stoweidlem7  31990  stoweidlem11  31994  stoweidlem13  31996  stoweidlem14  31997  stoweidlem26  32009  stoweidlem42  32025  stoweidlem52  32035  stoweidlem59  32042  stoweidlem60  32043  stoweidlem62  32045  wallispilem4  32051  wallispi  32053  stirlinglem1  32057  stirlinglem3  32059  stirlinglem6  32062  stirlinglem7  32063  stirlinglem10  32066  stirlinglem11  32067  dirkercncflem1  32086  dirkercncflem2  32087  fourierdlem10  32100  fourierdlem11  32101  fourierdlem12  32102  fourierdlem42  32132  fourierdlem47  32137  fourierdlem50  32140  fourierdlem51  32141  fourierdlem73  32163  fourierdlem79  32169  fourierdlem83  32173  fourierdlem103  32193  fourierdlem104  32194  sqwvfoura  32212  sqwvfourb  32213  fouriersw  32215  imo72b2  38557