Theorem ltletrd 10076

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  lelttrdi  10078  uzwo3  11659  rpgecl  11735  fznatpl1  12265  elfz1b  12279  modabs  12565  seqf1olem1  12702  expgt1  12760  leexp2a  12778  bernneq3  12854  expnbnd  12855  expmulnbnd  12858  digit1  12860  discr1  12862  hashfun  13084  seqcoll2  13106  abssubne0  13904  icodiamlt  14022  reccn2  14175  isercolllem1  14243  isumltss  14419  fprodntriv  14511  efcllem  14647  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  eirrlem  14771  rpnnen2lem11  14792  ruclem10  14807  bitsmod  14996  bitsinv1lem  15001  smuval2  15042  prmreclem5  15462  1arith  15469  2expltfac  15637  mndodconglem  17783  sylow1lem1  17836  gzrngunit  19631  nlmvscnlem1  22300  nrginvrcnlem  22305  iccpnfhmeo  22552  cnheibor  22562  evth  22566  lebnumlem1  22568  ipcnlem1  22852  lmnn  22869  ovolicc2lem2  23093  itg2monolem1  23323  itg2monolem3  23325  dvferm1lem  23551  dvcnvre  23586  dvfsumlem3  23595  dvfsumrlim  23598  plyco0  23752  aaliou2b  23900  pilem2  24010  cosordlem  24081  logdivlti  24170  logdivle  24172  logcnlem3  24190  logcnlem4  24191  cxpcn3lem  24288  atanre  24412  atanlogaddlem  24440  atans2  24458  ressatans  24461  birthdaylem3  24480  cxp2lim  24503  cxploglim2  24505  jensenlem2  24514  harmonicubnd  24536  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamucov  24564  ftalem2  24600  ftalem5  24603  vma1  24692  chtrpcl  24701  ppiltx  24703  fsumfldivdiaglem  24715  chtub  24737  fsumvma2  24739  chpval2  24743  chpchtsum  24744  chpub  24745  bpos1  24808  bposlem1  24809  bposlem2  24810  bposlem6  24814  gausslemma2dlem0c  24883  lgsquadlem1  24905  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chto1ub  24965  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  rplogsumlem2  24974  dchrisumlema  24977  dchrisumlem3  24980  dchrmusumlema  24982  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0lema  25003  mulog2sumlem1  25023  chpdifbndlem1  25042  chpdifbnd  25044  pntrsumo1  25054  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemb  25086  pntlemh  25088  pntlemr  25091  pntlem3  25098  pnt2  25102  ostth2lem1  25107  ostth2lem3  25124  ostth2lem4  25125  axsegconlem7  25603  axsegconlem10  25606  axlowdimlem16  25637  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  clwwlkn0  26302  clwlkisclwwlklem2a2  26308  clwwlkext2edg  26330  frgraregord013  26645  smatrcl  29190  1smat1  29198  lmdvg  29327  dya2icoseg  29666  eulerpartlems  29749  subfacval3  30425  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem14  31686  knoppndvlem18  31690  poimirlem7  32586  poimirlem24  32603  poimirlem29  32608  mblfinlem2  32617  itg2addnclem  32631  itg2addnclem3  32633  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anc  32663  areacirclem5  32674  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pell14qrgapw  36458  pellqrex  36461  pellfundgt1  36465  pellfundex  36468  ltrmxnn0  36534  jm2.24nn  36544  jm2.17c  36547  jm2.24  36548  jm2.23  36581  jm3.1lem1  36602  jm3.1lem2  36603  radcnvrat  37535  dstregt0  38434  monoords  38452  fsumnncl  38638  mullimc  38683  mullimcf  38690  sumnnodd  38697  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  limclner  38718  dvdivbd  38813  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  iblspltprt  38865  itgspltprt  38871  stoweidlem11  38904  stoweidlem24  38917  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem36  38929  stoweidlem42  38935  stoweidlem44  38937  stoweidlem51  38944  stoweidlem59  38952  wallispi  38963  wallispi2lem1  38964  wallispi2  38966  stirlinglem11  38977  dirkertrigeqlem1  38991  dirkeritg  38995  fourierdlem10  39010  fourierdlem11  39011  fourierdlem12  39012  fourierdlem15  39015  fourierdlem19  39019  fourierdlem20  39020  fourierdlem30  39030  fourierdlem32  39032  fourierdlem40  39040  fourierdlem41  39041  fourierdlem44  39044  fourierdlem46  39045  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem89  39088  fourierdlem92  39091  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  etransclem4  39131  etransclem23  39150  etransclem31  39158  etransclem32  39159  etransclem35  39162  etransclem41  39168  etransclem48  39175  ioorrnopnlem  39200  sge0uzfsumgt  39337  sge0seq  39339  iundjiun  39353  carageniuncllem2  39412  hoidmvlelem3  39487  iunhoiioolem  39566  vonioolem1  39571  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  bgoldbtbndlem2  40222  clwlkclwwlklem2a2  41202  clwwlksext2edg  41230  logbpw2m1  42159