Theorem lttrd 9636

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1758   class class class wbr 4393   RRcr 9385   < clt 9522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-resscn 9443  ax-pre-lttrn 9461

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-er 7204  df-en 7414  df-dom 7415  df-sdom 7416  df-pnf 9524  df-mnf 9525  df-ltxr 9527

This theorem is referenced by:  expgt1  12012  ltexp2a  12025  expcan  12026  ltexp2  12027  leexp2  12028  expnlbnd2  12105  expmulnbnd  12106  reccn2  13185  efgt1  13511  tanhlt1  13555  ruclem2  13625  pythagtriplem13  14005  fldivp1  14070  4sqlem12  14128  sylow1lem1  16210  nrginvrcnlem  20396  iccntr  20523  icccmplem2  20525  opnreen  20533  pjthlem1  21049  pmltpclem2  21058  ovollb2lem  21096  opnmbllem  21207  volivth  21213  lhop1lem  21611  dvcnvrelem1  21615  dvcvx  21618  ftc1lem4  21637  aaliou3lem7  21941  ulmdvlem1  21991  reeff1olem  22037  pilem2  22043  pilem3  22044  tangtx  22093  tanord1  22119  tanord  22120  rplogcl  22179  logimul  22189  logcnlem3  22215  efopnlem1  22227  cxplt  22265  cxple  22266  cxpcn3lem  22311  asinsin  22413  atanlogaddlem  22434  atanlogsublem  22436  cxp2limlem  22495  cxp2lim  22496  ftalem1  22536  mersenne  22692  bposlem2  22750  bposlem6  22754  bposlem9  22757  lgsqrlem2  22807  lgsquadlem2  22820  chebbnd1lem2  22845  chebbnd1lem3  22846  chebbnd1  22847  chtppilimlem1  22848  chto1ub  22851  mulog2sumlem2  22910  chpdifbndlem1  22928  selberg3lem1  22932  pntrlog2bndlem2  22953  pntrlog2bndlem4  22955  pntpbnd1a  22960  pntpbnd1  22961  pntpbnd2  22962  pntibndlem1  22964  pntibndlem2  22966  pntibndlem3  22967  pntibnd  22968  pntlemb  22972  pntlemr  22977  pntlemf  22980  pnt  22989  ostth2lem1  22993  ostth2lem3  23010  ostth2lem4  23011  eupap1  23742  pjhthlem1  24939  sqsscirc1  26476  xrge0iifiso  26503  sgnsub  27064  signslema  27100  zetacvg  27138  lgamucov  27161  lgamcvg2  27178  opnmbllem0  28568  itg2gt0cn  28588  ftc1cnnclem  28606  ftc1anc  28616  cntotbnd  28836  pellexlem5  29315  pellfundex  29368  pellfundrp  29370  rmspecfund  29391  monotuz  29423  jm3.1lem2  29508  jm3.1lem3  29509  stoweidlem7  29943  stoweidlem11  29947  stoweidlem13  29949  stoweidlem14  29950  stoweidlem26  29962  stoweidlem42  29978  stoweidlem52  29988  stoweidlem59  29995  stoweidlem60  29996  stoweidlem62  29998  wallispilem4  30004  wallispi  30006  stirlinglem1  30010  stirlinglem3  30012  stirlinglem6  30015  stirlinglem7  30016  stirlinglem10  30019  stirlinglem11  30020  elfzom1elp1fzo  30359  wwlkext2clwwlk  30606  frgraogt3nreg  30854  friendshipgt3  30855  telescgsum  30958  chfacffsupp  31313  chfacfscmul0  31315  chfacfpmmul0  31319