Theorem ltletrd 11306

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185

This theorem is referenced by:  lelttrdi  11308  uzwo3  12893  rpgecl  12972  fznatpl1  13532  modabs  13863  seqf1olem1  14003  expgt1  14062  leexp2a  14134  bernneq3  14193  expnbnd  14194  expmulnbnd  14197  digit1  14199  discr1  14201  hashfun  14399  seqcoll2  14427  abssubne0  15279  icodiamlt  15400  reccn2  15559  isercolllem1  15627  isumltss  15813  fprodntriv  15907  efcllem  16042  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  eirrlem  16171  rpnnen2lem11  16191  ruclem10  16206  bitsmod  16405  bitsinv1lem  16410  smuval2  16451  prmreclem5  16891  1arith  16898  2expltfac  17063  mndodconglem  19516  sylow1lem1  19573  gzrngunit  21413  nlmvscnlem1  24651  nrginvrcnlem  24656  iccpnfhmeo  24912  cnheibor  24922  evth  24926  lebnumlem1  24928  ipcnlem1  25212  lmnn  25230  ovolicc2lem2  25485  itg2monolem1  25717  itg2monolem3  25719  dvferm1lem  25951  dvcnvre  25986  dvfsumlem3  25995  dvfsumrlim  25998  plyco0  26157  aaliou2b  26307  pilem2  26417  cosq34lt1  26491  cosordlem  26494  logdivlti  26584  logdivle  26586  logcnlem3  26608  logcnlem4  26609  cxpcn3lem  26711  atanre  26849  atanlogaddlem  26877  atans2  26895  birthdaylem3  26917  cxp2lim  26940  cxploglim2  26942  jensenlem2  26951  harmonicubnd  26973  fsumharmonic  26975  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamucov  27001  ftalem2  27037  ftalem5  27040  vma1  27129  chtrpcl  27138  ppiltx  27140  fsumfldivdiaglem  27152  chtub  27175  fsumvma2  27177  chpval2  27181  chpchtsum  27182  chpub  27183  bpos1  27246  bposlem1  27247  bposlem2  27248  bposlem6  27252  gausslemma2dlem0c  27321  lgsquadlem1  27343  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chto1ub  27439  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  rplogsumlem2  27448  dchrisumlema  27451  dchrisumlem3  27454  dchrmusumlema  27456  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0lema  27477  mulog2sumlem1  27497  chpdifbndlem1  27516  chpdifbnd  27518  pntrsumo1  27528  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2  27554  pntlemb  27560  pntlemh  27562  pntlemr  27565  pntlem3  27572  pnt2  27576  ostth2lem1  27581  ostth2lem3  27598  ostth2lem4  27599  axsegconlem7  28992  axsegconlem10  28995  axlowdimlem16  29026  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  clwlkclwwlklem2a2  30063  clwwlkext2edg  30126  smatrcl  33940  1smat1  33948  lmdvg  34097  dya2icoseg  34421  eulerpartlems  34504  reprlt  34763  reprinfz1  34766  breprexplemc  34776  hgt750lemd  34792  hgt750lem  34795  hgt750leme  34802  tgoldbachgtde  34804  subfacval3  35371  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem14  36785  knoppndvlem18  36789  poimirlem7  37948  poimirlem24  37965  poimirlem29  37970  mblfinlem2  37979  itg2addnclem  37992  itg2addnclem3  37994  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anc  38022  areacirclem5  38033  lcmineqlem23  42490  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  aks4d1lem1  42501  dvrelog2  42503  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8d2  42524  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  hashscontpow1  42560  aks6d1c3  42562  2ap1caineq  42584  sticksstones12a  42596  sticksstones22  42607  aks6d1c7lem1  42619  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem6  42631  aks5lem8  42640  flt4lem7  43092  3cubeslem1  43116  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pell14qrgapw  43304  pellqrex  43307  pellfundgt1  43311  pellfundex  43314  ltrmxnn0  43377  jm2.24nn  43387  jm2.17c  43390  jm2.24  43391  jm2.23  43424  jm3.1lem1  43445  jm3.1lem2  43446  radcnvrat  44741  dstregt0  45715  monoords  45730  uzubioo  45995  fsumnncl  46002  mullimc  46046  mullimcf  46053  sumnnodd  46060  limcleqr  46072  addlimc  46076  0ellimcdiv  46077  limclner  46079  limsupgtlem  46205  dvdivbd  46351  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  stoweidlem11  46439  stoweidlem24  46452  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem36  46464  stoweidlem42  46470  stoweidlem44  46472  stoweidlem51  46479  stoweidlem59  46487  wallispi  46498  wallispi2lem1  46499  wallispi2  46501  stirlinglem11  46512  dirkertrigeqlem1  46526  dirkeritg  46530  fourierdlem10  46545  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem19  46554  fourierdlem20  46555  fourierdlem30  46565  fourierdlem32  46567  fourierdlem40  46575  fourierdlem41  46576  fourierdlem44  46579  fourierdlem46  46580  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem89  46623  fourierdlem92  46626  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  etransclem4  46666  etransclem23  46685  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem48  46710  ioorrnopnlem  46732  sge0uzfsumgt  46872  sge0seq  46874  iundjiun  46888  carageniuncllem2  46950  hoidmvlelem3  47025  iunhoiioolem  47103  vonioolem1  47108  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  ceilhalfgt1  47781  modm2nep1  47820  modp2nep1  47821  modm1nep2  47822  modm1nem2  47823  modm1p1ne  47824  bgoldbtbndlem2  48282  gpgprismgrusgra  48534  gpg3nbgrvtx0  48552  gpg3kgrtriexlem1  48559  logbpw2m1  49043