Theorem ltletrd 10802

Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
ltletrd.4	⊢ (𝜑 → 𝐴 < 𝐵)
ltletrd.5	⊢ (𝜑 → 𝐵 ≤ 𝐶)

Assertion

Ref	Expression
ltletrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem ltletrd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		ltletrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		ltletr 10734	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1367	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 697	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538   < clt 10677   ≤ cle 10678

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-pre-lttri 10613  ax-pre-lttrn 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683

This theorem is referenced by:  lelttrdi  10804  uzwo3  12346  rpgecl  12420  fznatpl1  12964  modabs  13275  seqf1olem1  13412  expgt1  13470  leexp2a  13539  bernneq3  13595  expnbnd  13596  expmulnbnd  13599  digit1  13601  discr1  13603  hashfun  13801  seqcoll2  13826  abssubne0  14678  icodiamlt  14797  reccn2  14955  isercolllem1  15023  isumltss  15205  fprodntriv  15298  efcllem  15433  sin01bnd  15540  cos01bnd  15541  sin01gt0  15545  eirrlem  15559  rpnnen2lem11  15579  ruclem10  15594  bitsmod  15787  bitsinv1lem  15792  smuval2  15833  prmreclem5  16258  1arith  16265  2expltfac  16428  mndodconglem  18671  sylow1lem1  18725  gzrngunit  20613  nlmvscnlem1  23297  nrginvrcnlem  23302  iccpnfhmeo  23551  cnheibor  23561  evth  23565  lebnumlem1  23567  ipcnlem1  23850  lmnn  23868  ovolicc2lem2  24121  itg2monolem1  24353  itg2monolem3  24355  dvferm1lem  24583  dvcnvre  24618  dvfsumlem3  24627  dvfsumrlim  24630  plyco0  24784  aaliou2b  24932  pilem2  25042  cosq34lt1  25114  cosordlem  25117  logdivlti  25205  logdivle  25207  logcnlem3  25229  logcnlem4  25230  cxpcn3lem  25330  atanre  25465  atanlogaddlem  25493  atans2  25511  birthdaylem3  25533  cxp2lim  25556  cxploglim2  25558  jensenlem2  25567  harmonicubnd  25589  fsumharmonic  25591  lgamgulmlem2  25609  lgamgulmlem3  25610  lgamucov  25617  ftalem2  25653  ftalem5  25656  vma1  25745  chtrpcl  25754  ppiltx  25756  fsumfldivdiaglem  25768  chtub  25790  fsumvma2  25792  chpval2  25796  chpchtsum  25797  chpub  25798  bpos1  25861  bposlem1  25862  bposlem2  25863  bposlem6  25867  gausslemma2dlem0c  25936  lgsquadlem1  25958  chebbnd1lem1  26047  chebbnd1lem2  26048  chebbnd1lem3  26049  chebbnd1  26050  chtppilimlem1  26051  chtppilimlem2  26052  chtppilim  26053  chto1ub  26054  chebbnd2  26055  chto1lb  26056  chpchtlim  26057  chpo1ub  26058  rplogsumlem2  26063  dchrisumlema  26066  dchrisumlem3  26069  dchrmusumlema  26071  dchrvmasumlem2  26076  dchrvmasumiflem1  26079  dchrisum0lema  26092  mulog2sumlem1  26112  chpdifbndlem1  26131  chpdifbnd  26133  pntrsumo1  26143  pntpbnd1  26164  pntpbnd2  26165  pntibndlem2  26169  pntlemb  26175  pntlemh  26177  pntlemr  26180  pntlem3  26187  pnt2  26191  ostth2lem1  26196  ostth2lem3  26213  ostth2lem4  26214  axsegconlem7  26711  axsegconlem10  26714  axlowdimlem16  26745  axcontlem2  26753  axcontlem4  26755  axcontlem7  26758  clwlkclwwlklem2a2  27773  clwwlkext2edg  27837  smatrcl  31063  1smat1  31071  lmdvg  31198  dya2icoseg  31537  eulerpartlems  31620  reprlt  31892  reprinfz1  31895  breprexplemc  31905  hgt750lemd  31921  hgt750lem  31924  hgt750leme  31931  tgoldbachgtde  31933  subfacval3  32438  knoppndvlem1  33853  knoppndvlem2  33854  knoppndvlem7  33859  knoppndvlem14  33866  knoppndvlem18  33870  poimirlem7  34901  poimirlem24  34918  poimirlem29  34923  mblfinlem2  34932  itg2addnclem  34945  itg2addnclem3  34947  ftc1anclem5  34973  ftc1anclem7  34975  ftc1anc  34977  areacirclem5  34988  3cubeslem1  39288  irrapxlem4  39429  irrapxlem5  39430  pellexlem2  39434  pell14qrgapw  39480  pellqrex  39483  pellfundgt1  39487  pellfundex  39490  ltrmxnn0  39553  jm2.24nn  39563  jm2.17c  39566  jm2.24  39567  jm2.23  39600  jm3.1lem1  39621  jm3.1lem2  39622  radcnvrat  40653  dstregt0  41554  monoords  41571  uzubioo  41850  fsumnncl  41859  mullimc  41904  mullimcf  41911  sumnnodd  41918  limcleqr  41932  addlimc  41936  0ellimcdiv  41937  limclner  41939  limsupgtlem  42065  dvdivbd  42215  ioodvbdlimc1lem1  42223  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnmul  42235  iblspltprt  42265  itgspltprt  42271  stoweidlem11  42303  stoweidlem24  42316  stoweidlem25  42317  stoweidlem26  42318  stoweidlem34  42326  stoweidlem36  42328  stoweidlem42  42334  stoweidlem44  42336  stoweidlem51  42343  stoweidlem59  42351  wallispi  42362  wallispi2lem1  42363  wallispi2  42365  stirlinglem11  42376  dirkertrigeqlem1  42390  dirkeritg  42394  fourierdlem10  42409  fourierdlem11  42410  fourierdlem12  42411  fourierdlem15  42414  fourierdlem19  42418  fourierdlem20  42419  fourierdlem30  42429  fourierdlem32  42431  fourierdlem40  42439  fourierdlem41  42440  fourierdlem44  42443  fourierdlem46  42444  fourierdlem47  42445  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem79  42477  fourierdlem89  42487  fourierdlem92  42490  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  etransclem4  42530  etransclem23  42549  etransclem31  42557  etransclem32  42558  etransclem35  42561  etransclem41  42567  etransclem48  42574  ioorrnopnlem  42596  sge0uzfsumgt  42733  sge0seq  42735  iundjiun  42749  carageniuncllem2  42811  hoidmvlelem3  42886  iunhoiioolem  42964  vonioolem1  42969  smfmullem1  43073  smfmullem2  43074  smfmullem3  43075  bgoldbtbndlem2  43978  logbpw2m1  44634