Theorem ltletrd 11065

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946

This theorem is referenced by:  lelttrdi  11067  uzwo3  12612  rpgecl  12687  fznatpl1  13239  modabs  13552  seqf1olem1  13690  expgt1  13749  leexp2a  13818  bernneq3  13874  expnbnd  13875  expmulnbnd  13878  digit1  13880  discr1  13882  hashfun  14080  seqcoll2  14107  abssubne0  14956  icodiamlt  15075  reccn2  15234  isercolllem1  15304  isumltss  15488  fprodntriv  15580  efcllem  15715  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  eirrlem  15841  rpnnen2lem11  15861  ruclem10  15876  bitsmod  16071  bitsinv1lem  16076  smuval2  16117  prmreclem5  16549  1arith  16556  2expltfac  16722  mndodconglem  19064  sylow1lem1  19118  gzrngunit  20576  nlmvscnlem1  23756  nrginvrcnlem  23761  iccpnfhmeo  24014  cnheibor  24024  evth  24028  lebnumlem1  24030  ipcnlem1  24314  lmnn  24332  ovolicc2lem2  24587  itg2monolem1  24820  itg2monolem3  24822  dvferm1lem  25053  dvcnvre  25088  dvfsumlem3  25097  dvfsumrlim  25100  plyco0  25258  aaliou2b  25406  pilem2  25516  cosq34lt1  25588  cosordlem  25591  logdivlti  25680  logdivle  25682  logcnlem3  25704  logcnlem4  25705  cxpcn3lem  25805  atanre  25940  atanlogaddlem  25968  atans2  25986  birthdaylem3  26008  cxp2lim  26031  cxploglim2  26033  jensenlem2  26042  harmonicubnd  26064  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamucov  26092  ftalem2  26128  ftalem5  26131  vma1  26220  chtrpcl  26229  ppiltx  26231  fsumfldivdiaglem  26243  chtub  26265  fsumvma2  26267  chpval2  26271  chpchtsum  26272  chpub  26273  bpos1  26336  bposlem1  26337  bposlem2  26338  bposlem6  26342  gausslemma2dlem0c  26411  lgsquadlem1  26433  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chto1ub  26529  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ub  26533  rplogsumlem2  26538  dchrisumlema  26541  dchrisumlem3  26544  dchrmusumlema  26546  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0lema  26567  mulog2sumlem1  26587  chpdifbndlem1  26606  chpdifbnd  26608  pntrsumo1  26618  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntlemb  26650  pntlemh  26652  pntlemr  26655  pntlem3  26662  pnt2  26666  ostth2lem1  26671  ostth2lem3  26688  ostth2lem4  26689  axsegconlem7  27194  axsegconlem10  27197  axlowdimlem16  27228  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  clwlkclwwlklem2a2  28258  clwwlkext2edg  28321  smatrcl  31648  1smat1  31656  lmdvg  31805  dya2icoseg  32144  eulerpartlems  32227  reprlt  32499  reprinfz1  32502  breprexplemc  32512  hgt750lemd  32528  hgt750lem  32531  hgt750leme  32538  tgoldbachgtde  32540  subfacval3  33051  knoppndvlem1  34619  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem14  34632  knoppndvlem18  34636  poimirlem7  35711  poimirlem24  35728  poimirlem29  35733  mblfinlem2  35742  itg2addnclem  35755  itg2addnclem3  35757  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anc  35785  areacirclem5  35796  lcmineqlem23  39987  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  aks4d1lem1  39998  dvrelog2  40000  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  2ap1caineq  40029  sticksstones12a  40041  sticksstones22  40052  metakunt6  40058  metakunt11  40063  metakunt27  40079  metakunt28  40080  flt4lem7  40412  3cubeslem1  40422  irrapxlem4  40563  irrapxlem5  40564  pellexlem2  40568  pell14qrgapw  40614  pellqrex  40617  pellfundgt1  40621  pellfundex  40624  ltrmxnn0  40687  jm2.24nn  40697  jm2.17c  40700  jm2.24  40701  jm2.23  40734  jm3.1lem1  40755  jm3.1lem2  40756  radcnvrat  41821  dstregt0  42709  monoords  42726  uzubioo  42995  fsumnncl  43003  mullimc  43047  mullimcf  43054  sumnnodd  43061  limcleqr  43075  addlimc  43079  0ellimcdiv  43080  limclner  43082  limsupgtlem  43208  dvdivbd  43354  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  iblspltprt  43404  itgspltprt  43410  stoweidlem11  43442  stoweidlem24  43455  stoweidlem25  43456  stoweidlem26  43457  stoweidlem34  43465  stoweidlem36  43467  stoweidlem42  43473  stoweidlem44  43475  stoweidlem51  43482  stoweidlem59  43490  wallispi  43501  wallispi2lem1  43502  wallispi2  43504  stirlinglem11  43515  dirkertrigeqlem1  43529  dirkeritg  43533  fourierdlem10  43548  fourierdlem11  43549  fourierdlem12  43550  fourierdlem15  43553  fourierdlem19  43557  fourierdlem20  43558  fourierdlem30  43568  fourierdlem32  43570  fourierdlem40  43578  fourierdlem41  43579  fourierdlem44  43582  fourierdlem46  43583  fourierdlem47  43584  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem79  43616  fourierdlem89  43626  fourierdlem92  43629  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  etransclem4  43669  etransclem23  43688  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem48  43713  ioorrnopnlem  43735  sge0uzfsumgt  43872  sge0seq  43874  iundjiun  43888  carageniuncllem2  43950  hoidmvlelem3  44025  iunhoiioolem  44103  vonioolem1  44108  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  bgoldbtbndlem2  45146  logbpw2m1  45801