Theorem lttrd 11311

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttrn 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189

This theorem is referenced by:  mulgt1  12020  nnne0  12196  neglt  12947  expgt1  14041  ltexp2a  14107  expcan  14110  ltexp2  14111  leexp2  14112  expnlbnd2  14175  expmulnbnd  14176  reccn2  15539  efgt1  16060  tanhlt1  16104  ruclem2  16176  isprm7  16654  pythagtriplem13  16774  fldivp1  16844  4sqlem12  16903  sylow1lem1  19504  telgsums  19899  chfacffsupp  22719  chfacfscmul0  22721  chfacfpmmul0  22725  nrginvrcnlem  24555  iccntr  24686  icccmplem2  24688  opnreen  24696  pjthlem1  25313  pmltpclem2  25326  ovollb2lem  25365  opnmbllem  25478  volivth  25484  lhop1lem  25894  dvcnvrelem1  25898  dvcvx  25901  ftc1lem4  25922  aaliou3lem7  26233  ulmdvlem1  26285  reeff1olem  26332  pilem2  26338  pilem3  26339  tangtx  26390  tanord1  26422  tanord  26423  rplogcl  26489  logimul  26499  logcnlem3  26529  efopnlem1  26541  cxplt  26579  cxple  26580  cxpcn3lem  26633  asinsin  26778  atanlogaddlem  26799  atanlogsublem  26801  cxp2limlem  26862  cxp2lim  26863  zetacvg  26901  lgamucov  26924  lgamcvg2  26941  ftalem1  26959  mersenne  27114  bposlem2  27172  bposlem6  27176  bposlem9  27179  lgsqrlem2  27234  lgsquadlem2  27268  chebbnd1lem2  27357  chebbnd1lem3  27358  chebbnd1  27359  chtppilimlem1  27360  chto1ub  27363  mulog2sumlem2  27422  chpdifbndlem1  27440  selberg3lem1  27444  pntrlog2bndlem2  27465  pntrlog2bndlem4  27467  pntpbnd1a  27472  pntpbnd1  27473  pntpbnd2  27474  pntibndlem1  27476  pntibndlem2  27478  pntibndlem3  27479  pntibnd  27480  pntlemb  27484  pntlemr  27489  pntlemf  27492  pnt  27501  ostth2lem1  27505  ostth2lem3  27522  ostth2lem4  27523  wwlksext2clwwlk  29959  frgrogt3nreg  30299  friendshipgt3  30300  pjhthlem1  31293  sgnsub  32735  chnub  32911  psgnfzto1stlem  33030  1smat1  33767  sqsscirc1  33871  xrge0iifiso  33898  signslema  34526  chtvalz  34593  hgt750lemd  34612  knoppndvlem12  36484  knoppndvlem14  36486  knoppndvlem15  36487  knoppndvlem17  36489  knoppndvlem20  36492  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem15  37602  poimirlem20  37607  poimirlem28  37615  opnmbllem0  37623  itg2gt0cn  37642  ftc1cnnclem  37658  ftc1anc  37668  cntotbnd  37763  3lexlogpow5ineq3  42018  3lexlogpow2ineq2  42020  3lexlogpow5ineq5  42021  aks4d1lem1  42023  0nonelalab  42028  aks4d1p1p3  42030  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p2  42038  aks4d1p3  42039  aks4d1p6  42042  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8d3  42047  aks4d1p8  42048  2ap1caineq  42106  sticksstones1  42107  sn-addlt0d  42419  sn-addgt0d  42420  sn-mulgt1d  42440  fimgmcyc  42495  flt4lem7  42620  fltnlta  42624  pellexlem5  42794  pellfundex  42847  pellfundrp  42849  rmspecfund  42870  monotuz  42903  jm3.1lem2  42980  jm3.1lem3  42981  imo72b2  44134  prmunb2  44273  ltadd12dd  45312  infleinflem2  45340  sqrlearg  45524  lptre2pt  45611  0ellimcdiv  45620  limsup10exlem  45743  ioodvbdlimc1lem1  45902  iblspltprt  45944  itgspltprt  45950  stoweidlem7  45978  stoweidlem11  45982  stoweidlem13  45984  stoweidlem14  45985  stoweidlem26  45997  stoweidlem42  46013  stoweidlem52  46023  stoweidlem59  46030  stoweidlem60  46031  stoweidlem62  46033  wallispilem4  46039  wallispi  46041  stirlinglem1  46045  stirlinglem3  46047  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  dirkercncflem1  46074  dirkercncflem2  46075  fourierdlem10  46088  fourierdlem11  46089  fourierdlem12  46090  fourierdlem42  46120  fourierdlem47  46124  fourierdlem50  46127  fourierdlem51  46128  fourierdlem73  46150  fourierdlem79  46156  fourierdlem83  46160  fourierdlem103  46180  fourierdlem104  46181  sqwvfoura  46199  sqwvfourb  46200  fouriersw  46202  hoidmvlelem1  46566  hoiqssbllem2  46594  hspmbllem1  46597  pimrecltpos  46679  pimrecltneg  46695  smfaddlem1  46734  smflimlem3  46744  smflimlem4  46745  smfmullem1  46762  ormkglobd  46846  difmodm1lt  47333  fpprel2  47715  gpgedgvtx0  48025  gpgedgvtx1  48026  eenglngeehlnmlem2  48700