Theorem ltletrd 11385

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 11317	. . 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 2146   class class class wbr 5111  ℝcr 11114   < clt 11258   ≤ cle 11259

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-pre-lttri 11189  ax-pre-lttrn 11190

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264

This theorem is used by:  lelttrdi  11387  uzwo3  12983  rpgecl  13062  fznatpl1  13623  modabs  13955  seqf1olem1  14095  expgt1  14154  leexp2a  14226  bernneq3  14285  expnbnd  14286  expmulnbnd  14289  digit1  14291  discr1  14293  hashfun  14492  seqcoll2  14520  abssubne0  15392  icodiamlt  15513  reccn2  15672  isercolllem1  15740  isumltss  15925  fprodntriv  16019  efcllem  16153  sin01bnd  16263  cos01bnd  16264  sin01gt0  16268  eirrlem  16282  rpnnen2lem11  16302  ruclem10  16317  bitsmod  16516  bitsinv1lem  16521  smuval2  16562  prmreclem5  17002  1arith  17009  2expltfac  17174  mndodconglem  19655  sylow1lem1  19712  gzrngunit  21633  nlmvscnlem1  24894  nrginvrcnlem  24899  iccpnfhmeo  25155  cnheibor  25165  evth  25169  lebnumlem1  25171  ipcnlem1  25455  lmnn  25473  ovolicc2lem2  25728  itg2monolem1  25960  itg2monolem3  25962  dvferm1lem  26194  dvcnvre  26229  dvfsumlem3  26238  dvfsumrlim  26241  plyco0  26400  aaliou2b  26555  pilem2  26666  cosq34lt1  26743  cosordlem  26746  logdivlti  26836  logdivle  26838  logcnlem3  26860  logcnlem4  26861  cxpcn3lem  26963  atanre  27101  atanlogaddlem  27129  atans2  27147  birthdaylem3  27169  cxp2lim  27192  cxploglim2  27194  jensenlem2  27203  harmonicubnd  27225  fsumharmonic  27227  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamucov  27253  ftalem2  27289  ftalem5  27292  vma1  27381  chtrpcl  27390  ppiltx  27392  fsumfldivdiaglem  27404  chtub  27427  fsumvma2  27429  chpval2  27433  chpchtsum  27434  chpub  27435  bpos1  27498  bposlem1  27499  bposlem2  27500  bposlem6  27504  gausslemma2dlem0c  27573  lgsquadlem1  27595  chebbnd1lem1  27684  chebbnd1lem2  27685  chebbnd1lem3  27686  chebbnd1  27687  chtppilimlem1  27688  chtppilimlem2  27689  chtppilim  27690  chto1ub  27691  chebbnd2  27692  chto1lb  27693  chpchtlim  27694  chpo1ub  27695  rplogsumlem2  27700  dchrisumlema  27703  dchrisumlem3  27706  dchrmusumlema  27708  dchrvmasumlem2  27713  dchrvmasumiflem1  27716  dchrisum0lema  27729  mulog2sumlem1  27749  chpdifbndlem1  27768  chpdifbnd  27770  pntrsumo1  27780  pntpbnd1  27801  pntpbnd2  27802  pntibndlem2  27806  pntlemb  27812  pntlemh  27814  pntlemr  27817  pntlem3  27824  pnt2  27828  ostth2lem1  27833  ostth2lem3  27850  ostth2lem4  27851  axsegconlem7  29328  axsegconlem10  29331  axlowdimlem16  29362  axcontlem2  29370  axcontlem4  29372  axcontlem7  29375  clwlkclwwlklem2a2  30411  clwwlkext2edg  30474  smatrcl  34250  1smat1  34258  lmdvg  34407  dya2icoseg  34732  eulerpartlems  34815  reprlt  35071  reprinfz1  35074  breprexplemc  35084  hgt750lemd  35100  hgt750lem  35103  hgt750leme  35110  tgoldbachgtde  35112  subfacval3  35718  knoppndvlem1  37158  knoppndvlem2  37159  knoppndvlem7  37164  knoppndvlem14  37171  knoppndvlem18  37175  poimirlem7  38335  poimirlem24  38352  poimirlem29  38357  mblfinlem2  38366  itg2addnclem  38379  itg2addnclem3  38381  ftc1anclem5  38405  ftc1anclem7  38407  ftc1anc  38409  areacirclem5  38420  lcmineqlem23  42876  3lexlogpow5ineq2  42880  3lexlogpow5ineq4  42881  3lexlogpow5ineq3  42882  aks4d1lem1  42887  dvrelog2  42889  aks4d1p1p3  42894  aks4d1p1p2  42895  aks4d1p1p4  42896  aks4d1p1p6  42898  aks4d1p1p7  42899  aks4d1p1p5  42900  aks4d1p1  42901  aks4d1p2  42902  aks4d1p3  42903  aks4d1p5  42905  aks4d1p6  42906  aks4d1p7d1  42907  aks4d1p7  42908  aks4d1p8d2  42910  aks4d1p8  42912  aks4d1p9  42913  posbezout  42925  hashscontpow1  42946  aks6d1c3  42948  2ap1caineq  42970  sticksstones12a  42982  sticksstones22  42993  aks6d1c7lem1  43005  aks6d1c7lem2  43006  aks6d1c7  43009  aks5lem6  43017  aks5lem8  43026  flt4lem7  43449  3cubeslem1  43473  irrapxlem4  43610  irrapxlem5  43611  pellexlem2  43615  pell14qrgapw  43661  pellqrex  43664  pellfundgt1  43668  pellfundex  43671  ltrmxnn0  43734  jm2.24nn  43744  jm2.17c  43747  jm2.24  43748  jm2.23  43781  jm3.1lem1  43802  jm3.1lem2  43803  radcnvrat  45082  dstregt0  46059  monoords  46074  uzubioo  46339  fsumnncl  46346  mullimc  46390  mullimcf  46397  sumnnodd  46404  limcleqr  46416  addlimc  46420  0ellimcdiv  46421  limclner  46423  limsupgtlem  46549  dvdivbd  46695  ioodvbdlimc1lem1  46703  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  dvnmul  46715  iblspltprt  46745  itgspltprt  46751  stoweidlem11  46783  stoweidlem24  46796  stoweidlem25  46797  stoweidlem26  46798  stoweidlem34  46806  stoweidlem36  46808  stoweidlem42  46814  stoweidlem44  46816  stoweidlem51  46823  stoweidlem59  46831  wallispi  46842  wallispi2lem1  46843  wallispi2  46845  stirlinglem11  46856  dirkertrigeqlem1  46870  dirkeritg  46874  fourierdlem10  46889  fourierdlem11  46890  fourierdlem12  46891  fourierdlem15  46894  fourierdlem19  46898  fourierdlem20  46899  fourierdlem30  46909  fourierdlem32  46911  fourierdlem40  46919  fourierdlem41  46920  fourierdlem44  46923  fourierdlem46  46924  fourierdlem47  46925  fourierdlem48  46926  fourierdlem49  46927  fourierdlem50  46928  fourierdlem63  46941  fourierdlem64  46942  fourierdlem65  46943  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem78  46956  fourierdlem79  46957  fourierdlem89  46967  fourierdlem92  46970  fourierdlem103  46981  fourierdlem104  46982  fouriersw  47003  etransclem4  47010  etransclem23  47029  etransclem31  47037  etransclem32  47038  etransclem35  47041  etransclem41  47047  etransclem48  47054  ioorrnopnlem  47076  sge0uzfsumgt  47216  sge0seq  47218  iundjiun  47232  carageniuncllem2  47294  hoidmvlelem3  47369  iunhoiioolem  47447  vonioolem1  47452  smfmullem1  47563  smfmullem2  47564  smfmullem3  47565  ceilhalfgt1  48128  modm2nep1  48167  modp2nep1  48168  modm1nep2  48169  modm1nem2  48170  modm1p1ne  48171  bgoldbtbndlem2  48629  gpgprismgrusgra  48881  gpg3nbgrvtx0  48899  gpg3kgrtriexlem1  48906  logbpw2m1  49404