Theorem ltletrd 11341

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 11273	. . 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 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  lelttrdi  11343  uzwo3  12909  rpgecl  12988  fznatpl1  13546  modabs  13873  seqf1olem1  14013  expgt1  14072  leexp2a  14144  bernneq3  14203  expnbnd  14204  expmulnbnd  14207  digit1  14209  discr1  14211  hashfun  14409  seqcoll2  14437  abssubne0  15290  icodiamlt  15411  reccn2  15570  isercolllem1  15638  isumltss  15821  fprodntriv  15915  efcllem  16050  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  eirrlem  16179  rpnnen2lem11  16199  ruclem10  16214  bitsmod  16413  bitsinv1lem  16418  smuval2  16459  prmreclem5  16898  1arith  16905  2expltfac  17070  mndodconglem  19478  sylow1lem1  19535  gzrngunit  21357  nlmvscnlem1  24581  nrginvrcnlem  24586  iccpnfhmeo  24850  cnheibor  24861  evth  24865  lebnumlem1  24867  ipcnlem1  25152  lmnn  25170  ovolicc2lem2  25426  itg2monolem1  25658  itg2monolem3  25660  dvferm1lem  25895  dvcnvre  25931  dvfsumlem3  25942  dvfsumrlim  25945  plyco0  26104  aaliou2b  26256  pilem2  26369  cosq34lt1  26443  cosordlem  26446  logdivlti  26536  logdivle  26538  logcnlem3  26560  logcnlem4  26561  cxpcn3lem  26664  atanre  26802  atanlogaddlem  26830  atans2  26848  birthdaylem3  26870  cxp2lim  26894  cxploglim2  26896  jensenlem2  26905  harmonicubnd  26927  fsumharmonic  26929  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamucov  26955  ftalem2  26991  ftalem5  26994  vma1  27083  chtrpcl  27092  ppiltx  27094  fsumfldivdiaglem  27106  chtub  27130  fsumvma2  27132  chpval2  27136  chpchtsum  27137  chpub  27138  bpos1  27201  bposlem1  27202  bposlem2  27203  bposlem6  27207  gausslemma2dlem0c  27276  lgsquadlem1  27298  chebbnd1lem1  27387  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem1  27391  chtppilimlem2  27392  chtppilim  27393  chto1ub  27394  chebbnd2  27395  chto1lb  27396  chpchtlim  27397  chpo1ub  27398  rplogsumlem2  27403  dchrisumlema  27406  dchrisumlem3  27409  dchrmusumlema  27411  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0lema  27432  mulog2sumlem1  27452  chpdifbndlem1  27471  chpdifbnd  27473  pntrsumo1  27483  pntpbnd1  27504  pntpbnd2  27505  pntibndlem2  27509  pntlemb  27515  pntlemh  27517  pntlemr  27520  pntlem3  27527  pnt2  27531  ostth2lem1  27536  ostth2lem3  27553  ostth2lem4  27554  axsegconlem7  28857  axsegconlem10  28860  axlowdimlem16  28891  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  clwlkclwwlklem2a2  29929  clwwlkext2edg  29992  smatrcl  33793  1smat1  33801  lmdvg  33950  dya2icoseg  34275  eulerpartlems  34358  reprlt  34617  reprinfz1  34620  breprexplemc  34630  hgt750lemd  34646  hgt750lem  34649  hgt750leme  34656  tgoldbachgtde  34658  subfacval3  35183  knoppndvlem1  36507  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem14  36520  knoppndvlem18  36524  poimirlem7  37628  poimirlem24  37645  poimirlem29  37650  mblfinlem2  37659  itg2addnclem  37672  itg2addnclem3  37674  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anc  37702  areacirclem5  37713  lcmineqlem23  42046  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  aks4d1lem1  42057  dvrelog2  42059  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8d2  42080  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  hashscontpow1  42116  aks6d1c3  42118  2ap1caineq  42140  sticksstones12a  42152  sticksstones22  42163  aks6d1c7lem1  42175  aks6d1c7lem2  42176  aks6d1c7  42179  aks5lem6  42187  aks5lem8  42196  flt4lem7  42654  3cubeslem1  42679  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pell14qrgapw  42871  pellqrex  42874  pellfundgt1  42878  pellfundex  42881  ltrmxnn0  42945  jm2.24nn  42955  jm2.17c  42958  jm2.24  42959  jm2.23  42992  jm3.1lem1  43013  jm3.1lem2  43014  radcnvrat  44310  dstregt0  45287  monoords  45302  uzubioo  45570  fsumnncl  45577  mullimc  45621  mullimcf  45628  sumnnodd  45635  limcleqr  45649  addlimc  45653  0ellimcdiv  45654  limclner  45656  limsupgtlem  45782  dvdivbd  45928  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  iblspltprt  45978  itgspltprt  45984  stoweidlem11  46016  stoweidlem24  46029  stoweidlem25  46030  stoweidlem26  46031  stoweidlem34  46039  stoweidlem36  46041  stoweidlem42  46047  stoweidlem44  46049  stoweidlem51  46056  stoweidlem59  46064  wallispi  46075  wallispi2lem1  46076  wallispi2  46078  stirlinglem11  46089  dirkertrigeqlem1  46103  dirkeritg  46107  fourierdlem10  46122  fourierdlem11  46123  fourierdlem12  46124  fourierdlem15  46127  fourierdlem19  46131  fourierdlem20  46132  fourierdlem30  46142  fourierdlem32  46144  fourierdlem40  46152  fourierdlem41  46153  fourierdlem44  46156  fourierdlem46  46157  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem89  46200  fourierdlem92  46203  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  etransclem4  46243  etransclem23  46262  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem41  46280  etransclem48  46287  ioorrnopnlem  46309  sge0uzfsumgt  46449  sge0seq  46451  iundjiun  46465  carageniuncllem2  46527  hoidmvlelem3  46602  iunhoiioolem  46680  vonioolem1  46685  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  ceilhalfgt1  47334  modm2nep1  47371  modp2nep1  47372  modm1nep2  47373  modm1nem2  47374  modm1p1ne  47375  bgoldbtbndlem2  47811  gpgprismgrusgra  48053  gpg3nbgrvtx0  48071  gpg3kgrtriexlem1  48078  logbpw2m1  48560