Theorem ltletrd 11310

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 11242	. . 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   ≤ cle 11185

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-lttri 11118  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-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  lelttrdi  11312  uzwo3  12878  rpgecl  12957  fznatpl1  13515  modabs  13842  seqf1olem1  13982  expgt1  14041  leexp2a  14113  bernneq3  14172  expnbnd  14173  expmulnbnd  14176  digit1  14178  discr1  14180  hashfun  14378  seqcoll2  14406  abssubne0  15259  icodiamlt  15380  reccn2  15539  isercolllem1  15607  isumltss  15790  fprodntriv  15884  efcllem  16019  sin01bnd  16129  cos01bnd  16130  sin01gt0  16134  eirrlem  16148  rpnnen2lem11  16168  ruclem10  16183  bitsmod  16382  bitsinv1lem  16387  smuval2  16428  prmreclem5  16867  1arith  16874  2expltfac  17039  mndodconglem  19455  sylow1lem1  19512  gzrngunit  21375  nlmvscnlem1  24607  nrginvrcnlem  24612  iccpnfhmeo  24876  cnheibor  24887  evth  24891  lebnumlem1  24893  ipcnlem1  25178  lmnn  25196  ovolicc2lem2  25452  itg2monolem1  25684  itg2monolem3  25686  dvferm1lem  25921  dvcnvre  25957  dvfsumlem3  25968  dvfsumrlim  25971  plyco0  26130  aaliou2b  26282  pilem2  26395  cosq34lt1  26469  cosordlem  26472  logdivlti  26562  logdivle  26564  logcnlem3  26586  logcnlem4  26587  cxpcn3lem  26690  atanre  26828  atanlogaddlem  26856  atans2  26874  birthdaylem3  26896  cxp2lim  26920  cxploglim2  26922  jensenlem2  26931  harmonicubnd  26953  fsumharmonic  26955  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamucov  26981  ftalem2  27017  ftalem5  27020  vma1  27109  chtrpcl  27118  ppiltx  27120  fsumfldivdiaglem  27132  chtub  27156  fsumvma2  27158  chpval2  27162  chpchtsum  27163  chpub  27164  bpos1  27227  bposlem1  27228  bposlem2  27229  bposlem6  27233  gausslemma2dlem0c  27302  lgsquadlem1  27324  chebbnd1lem1  27413  chebbnd1lem2  27414  chebbnd1lem3  27415  chebbnd1  27416  chtppilimlem1  27417  chtppilimlem2  27418  chtppilim  27419  chto1ub  27420  chebbnd2  27421  chto1lb  27422  chpchtlim  27423  chpo1ub  27424  rplogsumlem2  27429  dchrisumlema  27432  dchrisumlem3  27435  dchrmusumlema  27437  dchrvmasumlem2  27442  dchrvmasumiflem1  27445  dchrisum0lema  27458  mulog2sumlem1  27478  chpdifbndlem1  27497  chpdifbnd  27499  pntrsumo1  27509  pntpbnd1  27530  pntpbnd2  27531  pntibndlem2  27535  pntlemb  27541  pntlemh  27543  pntlemr  27546  pntlem3  27553  pnt2  27557  ostth2lem1  27562  ostth2lem3  27579  ostth2lem4  27580  axsegconlem7  28903  axsegconlem10  28906  axlowdimlem16  28937  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  clwlkclwwlklem2a2  29972  clwwlkext2edg  30035  smatrcl  33779  1smat1  33787  lmdvg  33936  dya2icoseg  34261  eulerpartlems  34344  reprlt  34603  reprinfz1  34606  breprexplemc  34616  hgt750lemd  34632  hgt750lem  34635  hgt750leme  34642  tgoldbachgtde  34644  subfacval3  35169  knoppndvlem1  36493  knoppndvlem2  36494  knoppndvlem7  36499  knoppndvlem14  36506  knoppndvlem18  36510  poimirlem7  37614  poimirlem24  37631  poimirlem29  37636  mblfinlem2  37645  itg2addnclem  37658  itg2addnclem3  37660  ftc1anclem5  37684  ftc1anclem7  37686  ftc1anc  37688  areacirclem5  37699  lcmineqlem23  42032  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  aks4d1lem1  42043  dvrelog2  42045  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  hashscontpow1  42102  aks6d1c3  42104  2ap1caineq  42126  sticksstones12a  42138  sticksstones22  42149  aks6d1c7lem1  42161  aks6d1c7lem2  42162  aks6d1c7  42165  aks5lem6  42173  aks5lem8  42182  flt4lem7  42640  3cubeslem1  42665  irrapxlem4  42806  irrapxlem5  42807  pellexlem2  42811  pell14qrgapw  42857  pellqrex  42860  pellfundgt1  42864  pellfundex  42867  ltrmxnn0  42931  jm2.24nn  42941  jm2.17c  42944  jm2.24  42945  jm2.23  42978  jm3.1lem1  42999  jm3.1lem2  43000  radcnvrat  44296  dstregt0  45273  monoords  45288  uzubioo  45556  fsumnncl  45563  mullimc  45607  mullimcf  45614  sumnnodd  45621  limcleqr  45635  addlimc  45639  0ellimcdiv  45640  limclner  45642  limsupgtlem  45768  dvdivbd  45914  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  iblspltprt  45964  itgspltprt  45970  stoweidlem11  46002  stoweidlem24  46015  stoweidlem25  46016  stoweidlem26  46017  stoweidlem34  46025  stoweidlem36  46027  stoweidlem42  46033  stoweidlem44  46035  stoweidlem51  46042  stoweidlem59  46050  wallispi  46061  wallispi2lem1  46062  wallispi2  46064  stirlinglem11  46075  dirkertrigeqlem1  46089  dirkeritg  46093  fourierdlem10  46108  fourierdlem11  46109  fourierdlem12  46110  fourierdlem15  46113  fourierdlem19  46117  fourierdlem20  46118  fourierdlem30  46128  fourierdlem32  46130  fourierdlem40  46138  fourierdlem41  46139  fourierdlem44  46142  fourierdlem46  46143  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem89  46186  fourierdlem92  46189  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem4  46229  etransclem23  46248  etransclem31  46256  etransclem32  46257  etransclem35  46260  etransclem41  46266  etransclem48  46273  ioorrnopnlem  46295  sge0uzfsumgt  46435  sge0seq  46437  iundjiun  46451  carageniuncllem2  46513  hoidmvlelem3  46588  iunhoiioolem  46666  vonioolem1  46671  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  ceilhalfgt1  47323  modm2nep1  47360  modp2nep1  47361  modm1nep2  47362  modm1nem2  47363  modm1p1ne  47364  bgoldbtbndlem2  47800  gpgprismgrusgra  48042  gpg3nbgrvtx0  48060  gpg3kgrtriexlem1  48067  logbpw2m1  48549