Theorem ltletrd 11273

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005   < clt 11146   ≤ cle 11147

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152

This theorem is referenced by:  lelttrdi  11275  uzwo3  12841  rpgecl  12920  fznatpl1  13478  modabs  13808  seqf1olem1  13948  expgt1  14007  leexp2a  14079  bernneq3  14138  expnbnd  14139  expmulnbnd  14142  digit1  14144  discr1  14146  hashfun  14344  seqcoll2  14372  abssubne0  15224  icodiamlt  15345  reccn2  15504  isercolllem1  15572  isumltss  15755  fprodntriv  15849  efcllem  15984  sin01bnd  16094  cos01bnd  16095  sin01gt0  16099  eirrlem  16113  rpnnen2lem11  16133  ruclem10  16148  bitsmod  16347  bitsinv1lem  16352  smuval2  16393  prmreclem5  16832  1arith  16839  2expltfac  17004  mndodconglem  19453  sylow1lem1  19510  gzrngunit  21370  nlmvscnlem1  24601  nrginvrcnlem  24606  iccpnfhmeo  24870  cnheibor  24881  evth  24885  lebnumlem1  24887  ipcnlem1  25172  lmnn  25190  ovolicc2lem2  25446  itg2monolem1  25678  itg2monolem3  25680  dvferm1lem  25915  dvcnvre  25951  dvfsumlem3  25962  dvfsumrlim  25965  plyco0  26124  aaliou2b  26276  pilem2  26389  cosq34lt1  26463  cosordlem  26466  logdivlti  26556  logdivle  26558  logcnlem3  26580  logcnlem4  26581  cxpcn3lem  26684  atanre  26822  atanlogaddlem  26850  atans2  26868  birthdaylem3  26890  cxp2lim  26914  cxploglim2  26916  jensenlem2  26925  harmonicubnd  26947  fsumharmonic  26949  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamucov  26975  ftalem2  27011  ftalem5  27014  vma1  27103  chtrpcl  27112  ppiltx  27114  fsumfldivdiaglem  27126  chtub  27150  fsumvma2  27152  chpval2  27156  chpchtsum  27157  chpub  27158  bpos1  27221  bposlem1  27222  bposlem2  27223  bposlem6  27227  gausslemma2dlem0c  27296  lgsquadlem1  27318  chebbnd1lem1  27407  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  chtppilimlem1  27411  chtppilimlem2  27412  chtppilim  27413  chto1ub  27414  chebbnd2  27415  chto1lb  27416  chpchtlim  27417  chpo1ub  27418  rplogsumlem2  27423  dchrisumlema  27426  dchrisumlem3  27429  dchrmusumlema  27431  dchrvmasumlem2  27436  dchrvmasumiflem1  27439  dchrisum0lema  27452  mulog2sumlem1  27472  chpdifbndlem1  27491  chpdifbnd  27493  pntrsumo1  27503  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntlemb  27535  pntlemh  27537  pntlemr  27540  pntlem3  27547  pnt2  27551  ostth2lem1  27556  ostth2lem3  27573  ostth2lem4  27574  axsegconlem7  28901  axsegconlem10  28904  axlowdimlem16  28935  axcontlem2  28943  axcontlem4  28945  axcontlem7  28948  clwlkclwwlklem2a2  29973  clwwlkext2edg  30036  smatrcl  33809  1smat1  33817  lmdvg  33966  dya2icoseg  34290  eulerpartlems  34373  reprlt  34632  reprinfz1  34635  breprexplemc  34645  hgt750lemd  34661  hgt750lem  34664  hgt750leme  34671  tgoldbachgtde  34673  subfacval3  35233  knoppndvlem1  36554  knoppndvlem2  36555  knoppndvlem7  36560  knoppndvlem14  36567  knoppndvlem18  36571  poimirlem7  37675  poimirlem24  37692  poimirlem29  37697  mblfinlem2  37706  itg2addnclem  37719  itg2addnclem3  37721  ftc1anclem5  37745  ftc1anclem7  37747  ftc1anc  37749  areacirclem5  37760  lcmineqlem23  42092  3lexlogpow5ineq2  42096  3lexlogpow5ineq4  42097  3lexlogpow5ineq3  42098  aks4d1lem1  42103  dvrelog2  42105  aks4d1p1p3  42110  aks4d1p1p2  42111  aks4d1p1p4  42112  aks4d1p1p6  42114  aks4d1p1p7  42115  aks4d1p1p5  42116  aks4d1p1  42117  aks4d1p2  42118  aks4d1p3  42119  aks4d1p5  42121  aks4d1p6  42122  aks4d1p7d1  42123  aks4d1p7  42124  aks4d1p8d2  42126  aks4d1p8  42128  aks4d1p9  42129  posbezout  42141  hashscontpow1  42162  aks6d1c3  42164  2ap1caineq  42186  sticksstones12a  42198  sticksstones22  42209  aks6d1c7lem1  42221  aks6d1c7lem2  42222  aks6d1c7  42225  aks5lem6  42233  aks5lem8  42242  flt4lem7  42700  3cubeslem1  42725  irrapxlem4  42866  irrapxlem5  42867  pellexlem2  42871  pell14qrgapw  42917  pellqrex  42920  pellfundgt1  42924  pellfundex  42927  ltrmxnn0  42990  jm2.24nn  43000  jm2.17c  43003  jm2.24  43004  jm2.23  43037  jm3.1lem1  43058  jm3.1lem2  43059  radcnvrat  44355  dstregt0  45331  monoords  45346  uzubioo  45613  fsumnncl  45620  mullimc  45664  mullimcf  45671  sumnnodd  45678  limcleqr  45690  addlimc  45694  0ellimcdiv  45695  limclner  45697  limsupgtlem  45823  dvdivbd  45969  ioodvbdlimc1lem1  45977  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  dvnmul  45989  iblspltprt  46019  itgspltprt  46025  stoweidlem11  46057  stoweidlem24  46070  stoweidlem25  46071  stoweidlem26  46072  stoweidlem34  46080  stoweidlem36  46082  stoweidlem42  46088  stoweidlem44  46090  stoweidlem51  46097  stoweidlem59  46105  wallispi  46116  wallispi2lem1  46117  wallispi2  46119  stirlinglem11  46130  dirkertrigeqlem1  46144  dirkeritg  46148  fourierdlem10  46163  fourierdlem11  46164  fourierdlem12  46165  fourierdlem15  46168  fourierdlem19  46172  fourierdlem20  46173  fourierdlem30  46183  fourierdlem32  46185  fourierdlem40  46193  fourierdlem41  46194  fourierdlem44  46197  fourierdlem46  46198  fourierdlem47  46199  fourierdlem48  46200  fourierdlem49  46201  fourierdlem50  46202  fourierdlem63  46215  fourierdlem64  46216  fourierdlem65  46217  fourierdlem74  46226  fourierdlem75  46227  fourierdlem76  46228  fourierdlem78  46230  fourierdlem79  46231  fourierdlem89  46241  fourierdlem92  46244  fourierdlem103  46255  fourierdlem104  46256  fouriersw  46277  etransclem4  46284  etransclem23  46303  etransclem31  46311  etransclem32  46312  etransclem35  46315  etransclem41  46321  etransclem48  46328  ioorrnopnlem  46350  sge0uzfsumgt  46490  sge0seq  46492  iundjiun  46506  carageniuncllem2  46568  hoidmvlelem3  46643  iunhoiioolem  46721  vonioolem1  46726  smfmullem1  46837  smfmullem2  46838  smfmullem3  46839  ceilhalfgt1  47368  modm2nep1  47405  modp2nep1  47406  modm1nep2  47407  modm1nem2  47408  modm1p1ne  47409  bgoldbtbndlem2  47845  gpgprismgrusgra  48097  gpg3nbgrvtx0  48115  gpg3kgrtriexlem1  48122  logbpw2m1  48607