Theorem ltletrd 11463

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttri 11267  ax-pre-lttrn 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342

This theorem is used by:  lelttrdi  11465  uzwo3  13063  rpgecl  13143  fznatpl1  13705  modabs  14037  seqf1olem1  14177  expgt1  14236  leexp2a  14308  bernneq3  14368  expnbnd  14369  expmulnbnd  14372  digit1  14374  discr1  14376  hashfun  14575  seqcoll2  14603  abssubne0  15477  icodiamlt  15598  reccn2  15757  isercolllem1  15825  isumltss  16010  fprodntriv  16102  efcllem  16236  sin01bnd  16346  cos01bnd  16347  sin01gt0  16351  eirrlem  16365  rpnnen2lem11  16385  ruclem10  16400  bitsmod  16599  bitsinv1lem  16604  smuval2  16645  prmreclem5  17091  1arith  17098  2expltfac  17263  mndodconglem  19748  sylow1lem1  19805  gzrngunit  21732  nlmvscnlem1  24998  nrginvrcnlem  25003  iccpnfhmeo  25259  cnheibor  25269  evth  25273  lebnumlem1  25275  ipcnlem1  25559  lmnn  25577  ovolicc2lem2  25832  itg2monolem1  26064  itg2monolem3  26066  dvferm1lem  26297  dvcnvre  26332  dvfsumlem3  26341  dvfsumrlim  26344  plyco0  26503  aaliou2b  26661  pilem2  26772  cosq34lt1  26848  cosordlem  26851  logdivlti  26941  logdivle  26943  logcnlem3  26965  logcnlem4  26966  cxpcn3lem  27068  atanre  27206  atanlogaddlem  27234  atans2  27252  birthdaylem3  27274  cxp2lim  27297  cxploglim2  27299  jensenlem2  27308  harmonicubnd  27330  fsumharmonic  27332  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamucov  27358  ftalem2  27394  ftalem5  27397  vma1  27486  chtrpcl  27495  ppiltx  27497  fsumfldivdiaglem  27509  chtub  27532  fsumvma2  27534  chpval2  27538  chpchtsum  27539  chpub  27540  bpos1  27603  bposlem1  27604  bposlem2  27605  bposlem6  27609  gausslemma2dlem0c  27678  lgsquadlem1  27700  chebbnd1lem1  27789  chebbnd1lem2  27790  chebbnd1lem3  27791  chebbnd1  27792  chtppilimlem1  27793  chtppilimlem2  27794  chtppilim  27795  chto1ub  27796  chebbnd2  27797  chto1lb  27798  chpchtlim  27799  chpo1ub  27800  rplogsumlem2  27805  dchrisumlema  27808  dchrisumlem3  27811  dchrmusumlema  27813  dchrvmasumlem2  27818  dchrvmasumiflem1  27821  dchrisum0lema  27834  mulog2sumlem1  27854  chpdifbndlem1  27873  chpdifbnd  27875  pntrsumo1  27885  pntpbnd1  27906  pntpbnd2  27907  pntibndlem2  27911  pntlemb  27917  pntlemh  27919  pntlemr  27922  pntlem3  27929  pnt2  27933  ostth2lem1  27938  ostth2lem3  27955  ostth2lem4  27956  flt4lem7  27982  axsegconlem7  29494  axsegconlem10  29497  axlowdimlem16  29528  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  clwlkclwwlklem2a2  30577  clwwlkext2edg  30640  smatrcl  34421  1smat1  34429  lmdvg  34578  dya2icoseg  34902  eulerpartlems  34985  reprlt  35241  reprinfz1  35244  breprexplemc  35254  hgt750lemd  35270  hgt750lem  35273  hgt750leme  35280  tgoldbachgtde  35282  subfacval3  35933  knoppndvlem1  37358  knoppndvlem2  37359  knoppndvlem7  37364  knoppndvlem14  37371  knoppndvlem18  37375  poimirlem7  38525  poimirlem24  38542  poimirlem29  38547  mblfinlem2  38556  itg2addnclem  38569  itg2addnclem3  38571  ftc1anclem5  38595  ftc1anclem7  38597  ftc1anc  38599  areacirclem5  38610  lcmineqlem23  43081  3lexlogpow5ineq2  43085  3lexlogpow5ineq4  43086  3lexlogpow5ineq3  43087  aks4d1lem1  43092  dvrelog2  43094  aks4d1p1p3  43099  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p2  43107  aks4d1p3  43108  aks4d1p5  43110  aks4d1p6  43111  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8d2  43115  aks4d1p8  43117  aks4d1p9  43118  posbezout  43130  hashscontpow1  43151  aks6d1c3  43153  2ap1caineq  43175  sticksstones12a  43187  sticksstones22  43198  aks6d1c7lem1  43210  aks6d1c7lem2  43211  aks6d1c7  43214  aks5lem6  43222  aks5lem8  43231  3cubeslem1  43674  irrapxlem4  43811  irrapxlem5  43812  pellexlem2  43816  pell14qrgapw  43862  pellqrex  43865  pellfundgt1  43869  pellfundex  43872  ltrmxnn0  43935  jm2.24nn  43945  jm2.17c  43948  jm2.24  43949  jm2.23  43982  jm3.1lem1  44003  jm3.1lem2  44004  radcnvrat  45283  dstregt0  46267  monoords  46282  uzubioo  46546  fsumnncl  46553  mullimc  46597  mullimcf  46604  sumnnodd  46611  limcleqr  46623  addlimc  46627  0ellimcdiv  46628  limclner  46630  limsupgtlem  46756  dvdivbd  46902  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnmul  46922  iblspltprt  46952  itgspltprt  46958  stoweidlem11  46990  stoweidlem24  47003  stoweidlem25  47004  stoweidlem26  47005  stoweidlem34  47013  stoweidlem36  47015  stoweidlem42  47021  stoweidlem44  47023  stoweidlem51  47030  stoweidlem59  47038  wallispi  47049  wallispi2lem1  47050  wallispi2  47052  stirlinglem11  47063  dirkertrigeqlem1  47077  dirkeritg  47081  fourierdlem10  47096  fourierdlem11  47097  fourierdlem12  47098  fourierdlem15  47101  fourierdlem19  47105  fourierdlem20  47106  fourierdlem30  47116  fourierdlem32  47118  fourierdlem40  47126  fourierdlem41  47127  fourierdlem44  47130  fourierdlem46  47131  fourierdlem47  47132  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem78  47163  fourierdlem79  47164  fourierdlem89  47174  fourierdlem92  47177  fourierdlem103  47188  fourierdlem104  47189  fouriersw  47210  etransclem4  47217  etransclem23  47236  etransclem31  47244  etransclem32  47245  etransclem35  47248  etransclem41  47254  etransclem48  47261  ioorrnopnlem  47283  sge0uzfsumgt  47423  sge0seq  47425  iundjiun  47439  carageniuncllem2  47501  hoidmvlelem3  47576  iunhoiioolem  47654  vonioolem1  47659  smfmullem1  47770  smfmullem2  47771  smfmullem3  47772  ceilhalfgt1  48372  modm2nep1  48411  modp2nep1  48412  modm1nep2  48413  modm1nem2  48414  modm1p1ne  48415  bgoldbtbndlem2  48873  gpgprismgrusgra  49125  gpg3nbgrvtx0  49143  gpg3kgrtriexlem1  49150  logbpw2m1  49648