Theorem lttrd 11285

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5095  ℝcr 11016   < clt 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-pre-lttrn 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-ltxr 11162

This theorem is referenced by:  mulgt1  11994  nnne0  12170  neglt  12916  expgt1  14014  ltexp2a  14080  expcan  14083  ltexp2  14084  leexp2  14085  expnlbnd2  14148  expmulnbnd  14149  reccn2  15511  efgt1  16032  tanhlt1  16076  ruclem2  16148  isprm7  16626  pythagtriplem13  16746  fldivp1  16816  4sqlem12  16875  chnub  18536  chnccat  18540  sylow1lem1  19518  telgsums  19913  chfacffsupp  22791  chfacfscmul0  22793  chfacfpmmul0  22797  nrginvrcnlem  24626  iccntr  24757  icccmplem2  24759  opnreen  24767  pjthlem1  25384  pmltpclem2  25397  ovollb2lem  25436  opnmbllem  25549  volivth  25555  lhop1lem  25965  dvcnvrelem1  25969  dvcvx  25972  ftc1lem4  25993  aaliou3lem7  26304  ulmdvlem1  26356  reeff1olem  26403  pilem2  26409  pilem3  26410  tangtx  26461  tanord1  26493  tanord  26494  rplogcl  26560  logimul  26570  logcnlem3  26600  efopnlem1  26612  cxplt  26650  cxple  26651  cxpcn3lem  26704  asinsin  26849  atanlogaddlem  26870  atanlogsublem  26872  cxp2limlem  26933  cxp2lim  26934  zetacvg  26972  lgamucov  26995  lgamcvg2  27012  ftalem1  27030  mersenne  27185  bposlem2  27243  bposlem6  27247  bposlem9  27250  lgsqrlem2  27305  lgsquadlem2  27339  chebbnd1lem2  27428  chebbnd1lem3  27429  chebbnd1  27430  chtppilimlem1  27431  chto1ub  27434  mulog2sumlem2  27493  chpdifbndlem1  27511  selberg3lem1  27515  pntrlog2bndlem2  27536  pntrlog2bndlem4  27538  pntpbnd1a  27543  pntpbnd1  27544  pntpbnd2  27545  pntibndlem1  27547  pntibndlem2  27549  pntibndlem3  27550  pntibnd  27551  pntlemb  27555  pntlemr  27560  pntlemf  27563  pnt  27572  ostth2lem1  27576  ostth2lem3  27593  ostth2lem4  27594  wwlksext2clwwlk  30058  frgrogt3nreg  30398  friendshipgt3  30399  pjhthlem1  31392  sgnsub  32846  psgnfzto1stlem  33110  1smat1  33889  sqsscirc1  33993  xrge0iifiso  34020  signslema  34647  chtvalz  34714  hgt750lemd  34733  knoppndvlem12  36639  knoppndvlem14  36641  knoppndvlem15  36642  knoppndvlem17  36644  knoppndvlem20  36647  poimirlem6  37739  poimirlem7  37740  poimirlem8  37741  poimirlem15  37748  poimirlem20  37753  poimirlem28  37761  opnmbllem0  37769  itg2gt0cn  37788  ftc1cnnclem  37804  ftc1anc  37814  cntotbnd  37909  3lexlogpow5ineq3  42223  3lexlogpow2ineq2  42225  3lexlogpow5ineq5  42226  aks4d1lem1  42228  0nonelalab  42233  aks4d1p1p3  42235  aks4d1p1p2  42236  aks4d1p1p4  42237  aks4d1p1p6  42239  aks4d1p1p7  42240  aks4d1p1p5  42241  aks4d1p1  42242  aks4d1p2  42243  aks4d1p3  42244  aks4d1p6  42247  aks4d1p7d1  42248  aks4d1p7  42249  aks4d1p8d3  42252  aks4d1p8  42253  2ap1caineq  42311  sticksstones1  42312  sn-addlt0d  42628  sn-addgt0d  42629  sn-mulgt1d  42649  fimgmcyc  42704  flt4lem7  42817  fltnlta  42821  pellexlem5  42990  pellfundex  43043  pellfundrp  43045  rmspecfund  43066  monotuz  43098  jm3.1lem2  43175  jm3.1lem3  43176  imo72b2  44329  prmunb2  44468  ltadd12dd  45504  infleinflem2  45531  sqrlearg  45715  lptre2pt  45800  0ellimcdiv  45809  limsup10exlem  45932  ioodvbdlimc1lem1  46091  iblspltprt  46133  itgspltprt  46139  stoweidlem7  46167  stoweidlem11  46171  stoweidlem13  46173  stoweidlem14  46174  stoweidlem26  46186  stoweidlem42  46202  stoweidlem52  46212  stoweidlem59  46219  stoweidlem60  46220  stoweidlem62  46222  wallispilem4  46228  wallispi  46230  stirlinglem1  46234  stirlinglem3  46236  stirlinglem6  46239  stirlinglem7  46240  stirlinglem10  46243  stirlinglem11  46244  dirkercncflem1  46263  dirkercncflem2  46264  fourierdlem10  46277  fourierdlem11  46278  fourierdlem12  46279  fourierdlem42  46309  fourierdlem47  46313  fourierdlem50  46316  fourierdlem51  46317  fourierdlem73  46339  fourierdlem79  46345  fourierdlem83  46349  fourierdlem103  46369  fourierdlem104  46370  sqwvfoura  46388  sqwvfourb  46389  fouriersw  46391  hoidmvlelem1  46755  hoiqssbllem2  46783  hspmbllem1  46786  pimrecltpos  46868  pimrecltneg  46884  smfaddlem1  46923  smflimlem3  46933  smflimlem4  46934  smfmullem1  46951  ormkglobd  47035  chnsubseq  47040  difmodm1lt  47521  fpprel2  47903  gpgedgvtx0  48223  gpgedgvtx1  48224  eenglngeehlnmlem2  48900