Theorem lttrd 10800

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 10716	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1367	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 697	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110   class class class wbr 5065  ℝcr 10535   < clt 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-resscn 10593  ax-pre-lttrn 10611

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-ltxr 10679

This theorem is referenced by:  nnne0  11670  expgt1  13466  ltexp2a  13529  expcan  13532  ltexp2  13533  leexp2  13534  expnlbnd2  13594  expmulnbnd  13595  reccn2  14952  efgt1  15468  tanhlt1  15512  ruclem2  15584  isprm7  16051  pythagtriplem13  16163  fldivp1  16232  4sqlem12  16291  sylow1lem1  18722  telgsums  19112  chfacffsupp  21463  chfacfscmul0  21465  chfacfpmmul0  21469  nrginvrcnlem  23299  iccntr  23428  icccmplem2  23430  opnreen  23438  pjthlem1  24039  pmltpclem2  24049  ovollb2lem  24088  opnmbllem  24201  volivth  24207  lhop1lem  24609  dvcnvrelem1  24613  dvcvx  24616  ftc1lem4  24635  aaliou3lem7  24937  ulmdvlem1  24987  reeff1olem  25033  pilem2  25039  pilem3  25040  tangtx  25090  tanord1  25120  tanord  25121  rplogcl  25186  logimul  25196  logcnlem3  25226  efopnlem1  25238  cxplt  25276  cxple  25277  cxpcn3lem  25327  asinsin  25469  atanlogaddlem  25490  atanlogsublem  25492  cxp2limlem  25552  cxp2lim  25553  zetacvg  25591  lgamucov  25614  lgamcvg2  25631  ftalem1  25649  mersenne  25802  bposlem2  25860  bposlem6  25864  bposlem9  25867  lgsqrlem2  25922  lgsquadlem2  25956  chebbnd1lem2  26045  chebbnd1lem3  26046  chebbnd1  26047  chtppilimlem1  26048  chto1ub  26051  mulog2sumlem2  26110  chpdifbndlem1  26128  selberg3lem1  26132  pntrlog2bndlem2  26153  pntrlog2bndlem4  26155  pntpbnd1a  26160  pntpbnd1  26161  pntpbnd2  26162  pntibndlem1  26164  pntibndlem2  26166  pntibndlem3  26167  pntibnd  26168  pntlemb  26172  pntlemr  26177  pntlemf  26180  pnt  26189  ostth2lem1  26193  ostth2lem3  26210  ostth2lem4  26211  wwlksext2clwwlk  27835  frgrogt3nreg  28175  friendshipgt3  28176  pjhthlem1  29167  psgnfzto1stlem  30742  1smat1  31069  sqsscirc1  31151  xrge0iifiso  31178  sgnsub  31802  signslema  31832  chtvalz  31900  hgt750lemd  31919  knoppndvlem12  33862  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem20  33870  poimirlem6  34897  poimirlem7  34898  poimirlem8  34899  poimirlem15  34906  poimirlem20  34911  poimirlem28  34919  opnmbllem0  34927  itg2gt0cn  34946  ftc1cnnclem  34964  ftc1anc  34974  cntotbnd  35073  fltnlta  39273  pellexlem5  39428  pellfundex  39481  pellfundrp  39483  rmspecfund  39504  monotuz  39536  jm3.1lem2  39613  jm3.1lem3  39614  imo72b2  40523  prmunb2  40641  neglt  41548  ltadd12dd  41609  infleinflem2  41637  sqrlearg  41827  lptre2pt  41919  0ellimcdiv  41928  limsup10exlem  42051  ioodvbdlimc1lem1  42214  iblspltprt  42256  itgspltprt  42262  stoweidlem7  42291  stoweidlem11  42295  stoweidlem13  42297  stoweidlem14  42298  stoweidlem26  42310  stoweidlem42  42326  stoweidlem52  42336  stoweidlem59  42343  stoweidlem60  42344  stoweidlem62  42346  wallispilem4  42352  wallispi  42354  stirlinglem1  42358  stirlinglem3  42360  stirlinglem6  42363  stirlinglem7  42364  stirlinglem10  42367  stirlinglem11  42368  dirkercncflem1  42387  dirkercncflem2  42388  fourierdlem10  42401  fourierdlem11  42402  fourierdlem12  42403  fourierdlem42  42433  fourierdlem47  42437  fourierdlem50  42440  fourierdlem51  42441  fourierdlem73  42463  fourierdlem79  42469  fourierdlem83  42473  fourierdlem103  42493  fourierdlem104  42494  sqwvfoura  42512  sqwvfourb  42513  fouriersw  42515  hoidmvlelem1  42876  hoiqssbllem2  42904  hspmbllem1  42907  pimrecltpos  42986  pimrecltneg  43000  smfaddlem1  43038  smflimlem3  43048  smflimlem4  43049  smfmullem1  43065  fpprel2  43905  eenglngeehlnmlem2  44724