Theorem ltletrd 10800

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 10732	. . 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 5066  ℝcr 10536   < clt 10675   ≤ cle 10676

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 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612

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 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 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681

This theorem is referenced by:  lelttrdi  10802  uzwo3  12344  rpgecl  12418  fznatpl1  12962  modabs  13273  seqf1olem1  13410  expgt1  13468  leexp2a  13537  bernneq3  13593  expnbnd  13594  expmulnbnd  13597  digit1  13599  discr1  13601  hashfun  13799  seqcoll2  13824  abssubne0  14676  icodiamlt  14795  reccn2  14953  isercolllem1  15021  isumltss  15203  fprodntriv  15296  efcllem  15431  sin01bnd  15538  cos01bnd  15539  sin01gt0  15543  eirrlem  15557  rpnnen2lem11  15577  ruclem10  15592  bitsmod  15785  bitsinv1lem  15790  smuval2  15831  prmreclem5  16256  1arith  16263  2expltfac  16426  mndodconglem  18669  sylow1lem1  18723  gzrngunit  20611  nlmvscnlem1  23295  nrginvrcnlem  23300  iccpnfhmeo  23549  cnheibor  23559  evth  23563  lebnumlem1  23565  ipcnlem1  23848  lmnn  23866  ovolicc2lem2  24119  itg2monolem1  24351  itg2monolem3  24353  dvferm1lem  24581  dvcnvre  24616  dvfsumlem3  24625  dvfsumrlim  24628  plyco0  24782  aaliou2b  24930  pilem2  25040  cosq34lt1  25112  cosordlem  25115  logdivlti  25203  logdivle  25205  logcnlem3  25227  logcnlem4  25228  cxpcn3lem  25328  atanre  25463  atanlogaddlem  25491  atans2  25509  birthdaylem3  25531  cxp2lim  25554  cxploglim2  25556  jensenlem2  25565  harmonicubnd  25587  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamucov  25615  ftalem2  25651  ftalem5  25654  vma1  25743  chtrpcl  25752  ppiltx  25754  fsumfldivdiaglem  25766  chtub  25788  fsumvma2  25790  chpval2  25794  chpchtsum  25795  chpub  25796  bpos1  25859  bposlem1  25860  bposlem2  25861  bposlem6  25865  gausslemma2dlem0c  25934  lgsquadlem1  25956  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chto1ub  26052  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  rplogsumlem2  26061  dchrisumlema  26064  dchrisumlem3  26067  dchrmusumlema  26069  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0lema  26090  mulog2sumlem1  26110  chpdifbndlem1  26129  chpdifbnd  26131  pntrsumo1  26141  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntlemb  26173  pntlemh  26175  pntlemr  26178  pntlem3  26185  pnt2  26189  ostth2lem1  26194  ostth2lem3  26211  ostth2lem4  26212  axsegconlem7  26709  axsegconlem10  26712  axlowdimlem16  26743  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  clwlkclwwlklem2a2  27771  clwwlkext2edg  27835  smatrcl  31061  1smat1  31069  lmdvg  31196  dya2icoseg  31535  eulerpartlems  31618  reprlt  31890  reprinfz1  31893  breprexplemc  31903  hgt750lemd  31919  hgt750lem  31922  hgt750leme  31929  tgoldbachgtde  31931  subfacval3  32436  knoppndvlem1  33851  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem14  33864  knoppndvlem18  33868  poimirlem7  34914  poimirlem24  34931  poimirlem29  34936  mblfinlem2  34945  itg2addnclem  34958  itg2addnclem3  34960  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anc  34990  areacirclem5  35001  3cubeslem1  39330  irrapxlem4  39471  irrapxlem5  39472  pellexlem2  39476  pell14qrgapw  39522  pellqrex  39525  pellfundgt1  39529  pellfundex  39532  ltrmxnn0  39595  jm2.24nn  39605  jm2.17c  39608  jm2.24  39609  jm2.23  39642  jm3.1lem1  39663  jm3.1lem2  39664  radcnvrat  40695  dstregt0  41596  monoords  41613  uzubioo  41892  fsumnncl  41901  mullimc  41946  mullimcf  41953  sumnnodd  41960  limcleqr  41974  addlimc  41978  0ellimcdiv  41979  limclner  41981  limsupgtlem  42107  dvdivbd  42257  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnmul  42277  iblspltprt  42307  itgspltprt  42313  stoweidlem11  42345  stoweidlem24  42358  stoweidlem25  42359  stoweidlem26  42360  stoweidlem34  42368  stoweidlem36  42370  stoweidlem42  42376  stoweidlem44  42378  stoweidlem51  42385  stoweidlem59  42393  wallispi  42404  wallispi2lem1  42405  wallispi2  42407  stirlinglem11  42418  dirkertrigeqlem1  42432  dirkeritg  42436  fourierdlem10  42451  fourierdlem11  42452  fourierdlem12  42453  fourierdlem15  42456  fourierdlem19  42460  fourierdlem20  42461  fourierdlem30  42471  fourierdlem32  42473  fourierdlem40  42481  fourierdlem41  42482  fourierdlem44  42485  fourierdlem46  42486  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem89  42529  fourierdlem92  42532  fourierdlem103  42543  fourierdlem104  42544  fouriersw  42565  etransclem4  42572  etransclem23  42591  etransclem31  42599  etransclem32  42600  etransclem35  42603  etransclem41  42609  etransclem48  42616  ioorrnopnlem  42638  sge0uzfsumgt  42775  sge0seq  42777  iundjiun  42791  carageniuncllem2  42853  hoidmvlelem3  42928  iunhoiioolem  43006  vonioolem1  43011  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  bgoldbtbndlem2  44020  logbpw2m1  44676