Theorem lttrd 11066

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945

This theorem is referenced by:  nnne0  11937  expgt1  13749  ltexp2a  13812  expcan  13815  ltexp2  13816  leexp2  13817  expnlbnd2  13877  expmulnbnd  13878  reccn2  15234  efgt1  15753  tanhlt1  15797  ruclem2  15869  isprm7  16341  pythagtriplem13  16456  fldivp1  16526  4sqlem12  16585  sylow1lem1  19118  telgsums  19509  chfacffsupp  21913  chfacfscmul0  21915  chfacfpmmul0  21919  nrginvrcnlem  23761  iccntr  23890  icccmplem2  23892  opnreen  23900  pjthlem1  24506  pmltpclem2  24518  ovollb2lem  24557  opnmbllem  24670  volivth  24676  lhop1lem  25082  dvcnvrelem1  25086  dvcvx  25089  ftc1lem4  25108  aaliou3lem7  25414  ulmdvlem1  25464  reeff1olem  25510  pilem2  25516  pilem3  25517  tangtx  25567  tanord1  25598  tanord  25599  rplogcl  25664  logimul  25674  logcnlem3  25704  efopnlem1  25716  cxplt  25754  cxple  25755  cxpcn3lem  25805  asinsin  25947  atanlogaddlem  25968  atanlogsublem  25970  cxp2limlem  26030  cxp2lim  26031  zetacvg  26069  lgamucov  26092  lgamcvg2  26109  ftalem1  26127  mersenne  26280  bposlem2  26338  bposlem6  26342  bposlem9  26345  lgsqrlem2  26400  lgsquadlem2  26434  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chto1ub  26529  mulog2sumlem2  26588  chpdifbndlem1  26606  selberg3lem1  26610  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem1  26642  pntibndlem2  26644  pntibndlem3  26645  pntibnd  26646  pntlemb  26650  pntlemr  26655  pntlemf  26658  pnt  26667  ostth2lem1  26671  ostth2lem3  26688  ostth2lem4  26689  wwlksext2clwwlk  28322  frgrogt3nreg  28662  friendshipgt3  28663  pjhthlem1  29654  psgnfzto1stlem  31269  1smat1  31656  sqsscirc1  31760  xrge0iifiso  31787  sgnsub  32411  signslema  32441  chtvalz  32509  hgt750lemd  32528  knoppndvlem12  34630  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem20  34638  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem15  35719  poimirlem20  35724  poimirlem28  35732  opnmbllem0  35740  itg2gt0cn  35759  ftc1cnnclem  35775  ftc1anc  35785  cntotbnd  35881  3lexlogpow5ineq3  39993  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  0nonelalab  40003  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8d3  40022  aks4d1p8  40023  2ap1caineq  40029  sticksstones1  40030  flt4lem7  40412  fltnlta  40416  pellexlem5  40571  pellfundex  40624  pellfundrp  40626  rmspecfund  40647  monotuz  40679  jm3.1lem2  40756  jm3.1lem3  40757  imo72b2  41672  prmunb2  41818  neglt  42712  ltadd12dd  42772  infleinflem2  42800  sqrlearg  42981  lptre2pt  43071  0ellimcdiv  43080  limsup10exlem  43203  ioodvbdlimc1lem1  43362  iblspltprt  43404  itgspltprt  43410  stoweidlem7  43438  stoweidlem11  43442  stoweidlem13  43444  stoweidlem14  43445  stoweidlem26  43457  stoweidlem42  43473  stoweidlem52  43483  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  wallispilem4  43499  wallispi  43501  stirlinglem1  43505  stirlinglem3  43507  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  dirkercncflem1  43534  dirkercncflem2  43535  fourierdlem10  43548  fourierdlem11  43549  fourierdlem12  43550  fourierdlem42  43580  fourierdlem47  43584  fourierdlem50  43587  fourierdlem51  43588  fourierdlem73  43610  fourierdlem79  43616  fourierdlem83  43620  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  hoidmvlelem1  44023  hoiqssbllem2  44051  hspmbllem1  44054  pimrecltpos  44133  pimrecltneg  44147  smfaddlem1  44185  smflimlem3  44195  smflimlem4  44196  smfmullem1  44212  fpprel2  45081  eenglngeehlnmlem2  45972