Theorem ltletrd 11276

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   < clt 11149   ≤ cle 11150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155

This theorem is referenced by:  lelttrdi  11278  uzwo3  12844  rpgecl  12923  fznatpl1  13481  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  19420  sylow1lem1  19477  gzrngunit  21340  nlmvscnlem1  24572  nrginvrcnlem  24577  iccpnfhmeo  24841  cnheibor  24852  evth  24856  lebnumlem1  24858  ipcnlem1  25143  lmnn  25161  ovolicc2lem2  25417  itg2monolem1  25649  itg2monolem3  25651  dvferm1lem  25886  dvcnvre  25922  dvfsumlem3  25933  dvfsumrlim  25936  plyco0  26095  aaliou2b  26247  pilem2  26360  cosq34lt1  26434  cosordlem  26437  logdivlti  26527  logdivle  26529  logcnlem3  26551  logcnlem4  26552  cxpcn3lem  26655  atanre  26793  atanlogaddlem  26821  atans2  26839  birthdaylem3  26861  cxp2lim  26885  cxploglim2  26887  jensenlem2  26896  harmonicubnd  26918  fsumharmonic  26920  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamucov  26946  ftalem2  26982  ftalem5  26985  vma1  27074  chtrpcl  27083  ppiltx  27085  fsumfldivdiaglem  27097  chtub  27121  fsumvma2  27123  chpval2  27127  chpchtsum  27128  chpub  27129  bpos1  27192  bposlem1  27193  bposlem2  27194  bposlem6  27198  gausslemma2dlem0c  27267  lgsquadlem1  27289  chebbnd1lem1  27378  chebbnd1lem2  27379  chebbnd1lem3  27380  chebbnd1  27381  chtppilimlem1  27382  chtppilimlem2  27383  chtppilim  27384  chto1ub  27385  chebbnd2  27386  chto1lb  27387  chpchtlim  27388  chpo1ub  27389  rplogsumlem2  27394  dchrisumlema  27397  dchrisumlem3  27400  dchrmusumlema  27402  dchrvmasumlem2  27407  dchrvmasumiflem1  27410  dchrisum0lema  27423  mulog2sumlem1  27443  chpdifbndlem1  27462  chpdifbnd  27464  pntrsumo1  27474  pntpbnd1  27495  pntpbnd2  27496  pntibndlem2  27500  pntlemb  27506  pntlemh  27508  pntlemr  27511  pntlem3  27518  pnt2  27522  ostth2lem1  27527  ostth2lem3  27544  ostth2lem4  27545  axsegconlem7  28868  axsegconlem10  28871  axlowdimlem16  28902  axcontlem2  28910  axcontlem4  28912  axcontlem7  28915  clwlkclwwlklem2a2  29937  clwwlkext2edg  30000  smatrcl  33763  1smat1  33771  lmdvg  33920  dya2icoseg  34245  eulerpartlems  34328  reprlt  34587  reprinfz1  34590  breprexplemc  34600  hgt750lemd  34616  hgt750lem  34619  hgt750leme  34626  tgoldbachgtde  34628  subfacval3  35162  knoppndvlem1  36486  knoppndvlem2  36487  knoppndvlem7  36492  knoppndvlem14  36499  knoppndvlem18  36503  poimirlem7  37607  poimirlem24  37624  poimirlem29  37629  mblfinlem2  37638  itg2addnclem  37651  itg2addnclem3  37653  ftc1anclem5  37677  ftc1anclem7  37679  ftc1anc  37681  areacirclem5  37692  lcmineqlem23  42024  3lexlogpow5ineq2  42028  3lexlogpow5ineq4  42029  3lexlogpow5ineq3  42030  aks4d1lem1  42035  dvrelog2  42037  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8d2  42058  aks4d1p8  42060  aks4d1p9  42061  posbezout  42073  hashscontpow1  42094  aks6d1c3  42096  2ap1caineq  42118  sticksstones12a  42130  sticksstones22  42141  aks6d1c7lem1  42153  aks6d1c7lem2  42154  aks6d1c7  42157  aks5lem6  42165  aks5lem8  42174  flt4lem7  42632  3cubeslem1  42657  irrapxlem4  42798  irrapxlem5  42799  pellexlem2  42803  pell14qrgapw  42849  pellqrex  42852  pellfundgt1  42856  pellfundex  42859  ltrmxnn0  42922  jm2.24nn  42932  jm2.17c  42935  jm2.24  42936  jm2.23  42969  jm3.1lem1  42990  jm3.1lem2  42991  radcnvrat  44287  dstregt0  45264  monoords  45279  uzubioo  45546  fsumnncl  45553  mullimc  45597  mullimcf  45604  sumnnodd  45611  limcleqr  45625  addlimc  45629  0ellimcdiv  45630  limclner  45632  limsupgtlem  45758  dvdivbd  45904  ioodvbdlimc1lem1  45912  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  dvnmul  45924  iblspltprt  45954  itgspltprt  45960  stoweidlem11  45992  stoweidlem24  46005  stoweidlem25  46006  stoweidlem26  46007  stoweidlem34  46015  stoweidlem36  46017  stoweidlem42  46023  stoweidlem44  46025  stoweidlem51  46032  stoweidlem59  46040  wallispi  46051  wallispi2lem1  46052  wallispi2  46054  stirlinglem11  46065  dirkertrigeqlem1  46079  dirkeritg  46083  fourierdlem10  46098  fourierdlem11  46099  fourierdlem12  46100  fourierdlem15  46103  fourierdlem19  46107  fourierdlem20  46108  fourierdlem30  46118  fourierdlem32  46120  fourierdlem40  46128  fourierdlem41  46129  fourierdlem44  46132  fourierdlem46  46133  fourierdlem47  46134  fourierdlem48  46135  fourierdlem49  46136  fourierdlem50  46137  fourierdlem63  46150  fourierdlem64  46151  fourierdlem65  46152  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem78  46165  fourierdlem79  46166  fourierdlem89  46176  fourierdlem92  46179  fourierdlem103  46190  fourierdlem104  46191  fouriersw  46212  etransclem4  46219  etransclem23  46238  etransclem31  46246  etransclem32  46247  etransclem35  46250  etransclem41  46256  etransclem48  46263  ioorrnopnlem  46285  sge0uzfsumgt  46425  sge0seq  46427  iundjiun  46441  carageniuncllem2  46503  hoidmvlelem3  46578  iunhoiioolem  46656  vonioolem1  46661  smfmullem1  46772  smfmullem2  46773  smfmullem3  46774  ceilhalfgt1  47313  modm2nep1  47350  modp2nep1  47351  modm1nep2  47352  modm1nem2  47353  modm1p1ne  47354  bgoldbtbndlem2  47790  gpgprismgrusgra  48042  gpg3nbgrvtx0  48060  gpg3kgrtriexlem1  48067  logbpw2m1  48552