Theorem ltletrd 10538

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   class class class wbr 4888  ℝcr 10273   < clt 10413   ≤ cle 10414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-resscn 10331  ax-pre-lttri 10348  ax-pre-lttrn 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419

This theorem is referenced by:  lelttrdi  10540  uzwo3  12094  rpgecl  12171  fznatpl1  12716  modabs  13026  seqf1olem1  13162  expgt1  13220  leexp2a  13238  bernneq3  13315  expnbnd  13316  expmulnbnd  13319  digit1  13321  discr1  13323  hashfun  13542  seqcoll2  13567  abssubne0  14467  icodiamlt  14586  reccn2  14739  isercolllem1  14807  isumltss  14988  fprodntriv  15079  efcllem  15214  sin01bnd  15321  cos01bnd  15322  sin01gt0  15326  eirrlem  15340  rpnnen2lem11  15361  ruclem10  15376  bitsmod  15568  bitsinv1lem  15573  smuval2  15614  prmreclem5  16032  1arith  16039  2expltfac  16202  mndodconglem  18348  sylow1lem1  18401  gzrngunit  20212  nlmvscnlem1  22902  nrginvrcnlem  22907  iccpnfhmeo  23156  cnheibor  23166  evth  23170  lebnumlem1  23172  ipcnlem1  23455  lmnn  23473  ovolicc2lem2  23726  itg2monolem1  23958  itg2monolem3  23960  dvferm1lem  24188  dvcnvre  24223  dvfsumlem3  24232  dvfsumrlim  24235  plyco0  24389  aaliou2b  24537  pilem2  24647  cosordlem  24719  logdivlti  24807  logdivle  24809  logcnlem3  24831  logcnlem4  24832  cxpcn3lem  24932  atanre  25067  atanlogaddlem  25095  atans2  25113  ressatans  25116  birthdaylem3  25136  cxp2lim  25159  cxploglim2  25161  jensenlem2  25170  harmonicubnd  25192  fsumharmonic  25194  lgamgulmlem2  25212  lgamgulmlem3  25213  lgamucov  25220  ftalem2  25256  ftalem5  25259  vma1  25348  chtrpcl  25357  ppiltx  25359  fsumfldivdiaglem  25371  chtub  25393  fsumvma2  25395  chpval2  25399  chpchtsum  25400  chpub  25401  bpos1  25464  bposlem1  25465  bposlem2  25466  bposlem6  25470  gausslemma2dlem0c  25539  lgsquadlem1  25561  chebbnd1lem1  25614  chebbnd1lem2  25615  chebbnd1lem3  25616  chebbnd1  25617  chtppilimlem1  25618  chtppilimlem2  25619  chtppilim  25620  chto1ub  25621  chebbnd2  25622  chto1lb  25623  chpchtlim  25624  chpo1ub  25625  rplogsumlem2  25630  dchrisumlema  25633  dchrisumlem3  25636  dchrmusumlema  25638  dchrvmasumlem2  25643  dchrvmasumiflem1  25646  dchrisum0lema  25659  mulog2sumlem1  25679  chpdifbndlem1  25698  chpdifbnd  25700  pntrsumo1  25710  pntpbnd1  25731  pntpbnd2  25732  pntibndlem2  25736  pntlemb  25742  pntlemh  25744  pntlemr  25747  pntlem3  25754  pnt2  25758  ostth2lem1  25763  ostth2lem3  25780  ostth2lem4  25781  axsegconlem7  26276  axsegconlem10  26279  axlowdimlem16  26310  axcontlem2  26318  axcontlem4  26320  axcontlem7  26323  clwlkclwwlklem2a2  27377  clwwlkext2edg  27457  smatrcl  30464  1smat1  30472  lmdvg  30601  dya2icoseg  30941  eulerpartlems  31024  reprlt  31303  reprinfz1  31306  breprexplemc  31316  hgt750lemd  31332  hgt750lem  31335  hgt750leme  31342  tgoldbachgtde  31344  subfacval3  31774  knoppndvlem1  33089  knoppndvlem2  33090  knoppndvlem7  33095  knoppndvlem14  33102  knoppndvlem18  33106  poimirlem7  34047  poimirlem24  34064  poimirlem29  34069  mblfinlem2  34078  itg2addnclem  34091  itg2addnclem3  34093  ftc1anclem5  34119  ftc1anclem7  34121  ftc1anc  34123  areacirclem5  34134  irrapxlem4  38359  irrapxlem5  38360  pellexlem2  38364  pell14qrgapw  38410  pellqrex  38413  pellfundgt1  38417  pellfundex  38420  ltrmxnn0  38485  jm2.24nn  38495  jm2.17c  38498  jm2.24  38499  jm2.23  38532  jm3.1lem1  38553  jm3.1lem2  38554  radcnvrat  39479  dstregt0  40413  monoords  40430  uzubioo  40712  fsumnncl  40721  mullimc  40766  mullimcf  40773  sumnnodd  40780  limcleqr  40794  addlimc  40798  0ellimcdiv  40799  limclner  40801  limsupgtlem  40927  dvdivbd  41076  ioodvbdlimc1lem1  41084  ioodvbdlimc1lem2  41085  ioodvbdlimc2lem  41087  dvnmul  41096  iblspltprt  41126  itgspltprt  41132  stoweidlem11  41165  stoweidlem24  41178  stoweidlem25  41179  stoweidlem26  41180  stoweidlem34  41188  stoweidlem36  41190  stoweidlem42  41196  stoweidlem44  41198  stoweidlem51  41205  stoweidlem59  41213  wallispi  41224  wallispi2lem1  41225  wallispi2  41227  stirlinglem11  41238  dirkertrigeqlem1  41252  dirkeritg  41256  fourierdlem10  41271  fourierdlem11  41272  fourierdlem12  41273  fourierdlem15  41276  fourierdlem19  41280  fourierdlem20  41281  fourierdlem30  41291  fourierdlem32  41293  fourierdlem40  41301  fourierdlem41  41302  fourierdlem44  41305  fourierdlem46  41306  fourierdlem47  41307  fourierdlem48  41308  fourierdlem49  41309  fourierdlem50  41310  fourierdlem63  41323  fourierdlem64  41324  fourierdlem65  41325  fourierdlem74  41334  fourierdlem75  41335  fourierdlem76  41336  fourierdlem78  41338  fourierdlem79  41339  fourierdlem89  41349  fourierdlem92  41352  fourierdlem103  41363  fourierdlem104  41364  fouriersw  41385  etransclem4  41392  etransclem23  41411  etransclem31  41419  etransclem32  41420  etransclem35  41423  etransclem41  41429  etransclem48  41436  ioorrnopnlem  41458  sge0uzfsumgt  41595  sge0seq  41597  iundjiun  41611  carageniuncllem2  41673  hoidmvlelem3  41748  iunhoiioolem  41826  vonioolem1  41831  smfmullem1  41935  smfmullem2  41936  smfmullem3  41937  bgoldbtbndlem2  42729  logbpw2m1  43386