Theorem ltletrd 11381

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   class class class wbr 5148  ℝcr 11115   < clt 11255   ≤ cle 11256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-resscn 11173  ax-pre-lttri 11190  ax-pre-lttrn 11191

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261

This theorem is referenced by:  lelttrdi  11383  uzwo3  12934  rpgecl  13009  fznatpl1  13562  modabs  13876  seqf1olem1  14014  expgt1  14073  leexp2a  14144  bernneq3  14201  expnbnd  14202  expmulnbnd  14205  digit1  14207  discr1  14209  hashfun  14404  seqcoll2  14433  abssubne0  15270  icodiamlt  15389  reccn2  15548  isercolllem1  15618  isumltss  15801  fprodntriv  15893  efcllem  16028  sin01bnd  16135  cos01bnd  16136  sin01gt0  16140  eirrlem  16154  rpnnen2lem11  16174  ruclem10  16189  bitsmod  16384  bitsinv1lem  16389  smuval2  16430  prmreclem5  16860  1arith  16867  2expltfac  17033  mndodconglem  19457  sylow1lem1  19514  gzrngunit  21301  nlmvscnlem1  24524  nrginvrcnlem  24529  iccpnfhmeo  24791  cnheibor  24802  evth  24806  lebnumlem1  24808  ipcnlem1  25094  lmnn  25112  ovolicc2lem2  25368  itg2monolem1  25601  itg2monolem3  25603  dvferm1lem  25837  dvcnvre  25873  dvfsumlem3  25884  dvfsumrlim  25887  plyco0  26045  aaliou2b  26194  pilem2  26305  cosq34lt1  26377  cosordlem  26380  logdivlti  26469  logdivle  26471  logcnlem3  26493  logcnlem4  26494  cxpcn3lem  26597  atanre  26732  atanlogaddlem  26760  atans2  26778  birthdaylem3  26800  cxp2lim  26824  cxploglim2  26826  jensenlem2  26835  harmonicubnd  26857  fsumharmonic  26859  lgamgulmlem2  26877  lgamgulmlem3  26878  lgamucov  26885  ftalem2  26921  ftalem5  26924  vma1  27013  chtrpcl  27022  ppiltx  27024  fsumfldivdiaglem  27036  chtub  27060  fsumvma2  27062  chpval2  27066  chpchtsum  27067  chpub  27068  bpos1  27131  bposlem1  27132  bposlem2  27133  bposlem6  27137  gausslemma2dlem0c  27206  lgsquadlem1  27228  chebbnd1lem1  27317  chebbnd1lem2  27318  chebbnd1lem3  27319  chebbnd1  27320  chtppilimlem1  27321  chtppilimlem2  27322  chtppilim  27323  chto1ub  27324  chebbnd2  27325  chto1lb  27326  chpchtlim  27327  chpo1ub  27328  rplogsumlem2  27333  dchrisumlema  27336  dchrisumlem3  27339  dchrmusumlema  27341  dchrvmasumlem2  27346  dchrvmasumiflem1  27349  dchrisum0lema  27362  mulog2sumlem1  27382  chpdifbndlem1  27401  chpdifbnd  27403  pntrsumo1  27413  pntpbnd1  27434  pntpbnd2  27435  pntibndlem2  27439  pntlemb  27445  pntlemh  27447  pntlemr  27450  pntlem3  27457  pnt2  27461  ostth2lem1  27466  ostth2lem3  27483  ostth2lem4  27484  axsegconlem7  28616  axsegconlem10  28619  axlowdimlem16  28650  axcontlem2  28658  axcontlem4  28660  axcontlem7  28663  clwlkclwwlklem2a2  29681  clwwlkext2edg  29744  smatrcl  33242  1smat1  33250  lmdvg  33399  dya2icoseg  33742  eulerpartlems  33825  reprlt  34097  reprinfz1  34100  breprexplemc  34110  hgt750lemd  34126  hgt750lem  34129  hgt750leme  34136  tgoldbachgtde  34138  subfacval3  34646  knoppndvlem1  35855  knoppndvlem2  35856  knoppndvlem7  35861  knoppndvlem14  35868  knoppndvlem18  35872  poimirlem7  36962  poimirlem24  36979  poimirlem29  36984  mblfinlem2  36993  itg2addnclem  37006  itg2addnclem3  37008  ftc1anclem5  37032  ftc1anclem7  37034  ftc1anc  37036  areacirclem5  37047  lcmineqlem23  41386  3lexlogpow5ineq2  41390  3lexlogpow5ineq4  41391  3lexlogpow5ineq3  41392  aks4d1lem1  41397  dvrelog2  41399  aks4d1p1p3  41404  aks4d1p1p2  41405  aks4d1p1p4  41406  aks4d1p1p6  41408  aks4d1p1p7  41409  aks4d1p1p5  41410  aks4d1p1  41411  aks4d1p2  41412  aks4d1p3  41413  aks4d1p5  41415  aks4d1p6  41416  aks4d1p7d1  41417  aks4d1p7  41418  aks4d1p8d2  41420  aks4d1p8  41422  aks4d1p9  41423  2ap1caineq  41431  sticksstones12a  41443  sticksstones22  41454  metakunt6  41460  metakunt11  41465  metakunt27  41481  metakunt28  41482  flt4lem7  41867  3cubeslem1  41888  irrapxlem4  42029  irrapxlem5  42030  pellexlem2  42034  pell14qrgapw  42080  pellqrex  42083  pellfundgt1  42087  pellfundex  42090  ltrmxnn0  42154  jm2.24nn  42164  jm2.17c  42167  jm2.24  42168  jm2.23  42201  jm3.1lem1  42222  jm3.1lem2  42223  radcnvrat  43539  dstregt0  44453  monoords  44469  uzubioo  44742  fsumnncl  44750  mullimc  44794  mullimcf  44801  sumnnodd  44808  limcleqr  44822  addlimc  44826  0ellimcdiv  44827  limclner  44829  limsupgtlem  44955  dvdivbd  45101  ioodvbdlimc1lem1  45109  ioodvbdlimc1lem2  45110  ioodvbdlimc2lem  45112  dvnmul  45121  iblspltprt  45151  itgspltprt  45157  stoweidlem11  45189  stoweidlem24  45202  stoweidlem25  45203  stoweidlem26  45204  stoweidlem34  45212  stoweidlem36  45214  stoweidlem42  45220  stoweidlem44  45222  stoweidlem51  45229  stoweidlem59  45237  wallispi  45248  wallispi2lem1  45249  wallispi2  45251  stirlinglem11  45262  dirkertrigeqlem1  45276  dirkeritg  45280  fourierdlem10  45295  fourierdlem11  45296  fourierdlem12  45297  fourierdlem15  45300  fourierdlem19  45304  fourierdlem20  45305  fourierdlem30  45315  fourierdlem32  45317  fourierdlem40  45325  fourierdlem41  45326  fourierdlem44  45329  fourierdlem46  45330  fourierdlem47  45331  fourierdlem48  45332  fourierdlem49  45333  fourierdlem50  45334  fourierdlem63  45347  fourierdlem64  45348  fourierdlem65  45349  fourierdlem74  45358  fourierdlem75  45359  fourierdlem76  45360  fourierdlem78  45362  fourierdlem79  45363  fourierdlem89  45373  fourierdlem92  45376  fourierdlem103  45387  fourierdlem104  45388  fouriersw  45409  etransclem4  45416  etransclem23  45435  etransclem31  45443  etransclem32  45444  etransclem35  45447  etransclem41  45453  etransclem48  45460  ioorrnopnlem  45482  sge0uzfsumgt  45622  sge0seq  45624  iundjiun  45638  carageniuncllem2  45700  hoidmvlelem3  45775  iunhoiioolem  45853  vonioolem1  45858  smfmullem1  45969  smfmullem2  45970  smfmullem3  45971  bgoldbtbndlem2  46936  logbpw2m1  47418