Theorem ltletrd 11334

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 11266	. . 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 5107  ℝcr 11067   < clt 11208   ≤ cle 11209

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttri 11142  ax-pre-lttrn 11143

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  lelttrdi  11336  uzwo3  12902  rpgecl  12981  fznatpl1  13539  modabs  13866  seqf1olem1  14006  expgt1  14065  leexp2a  14137  bernneq3  14196  expnbnd  14197  expmulnbnd  14200  digit1  14202  discr1  14204  hashfun  14402  seqcoll2  14430  abssubne0  15283  icodiamlt  15404  reccn2  15563  isercolllem1  15631  isumltss  15814  fprodntriv  15908  efcllem  16043  sin01bnd  16153  cos01bnd  16154  sin01gt0  16158  eirrlem  16172  rpnnen2lem11  16192  ruclem10  16207  bitsmod  16406  bitsinv1lem  16411  smuval2  16452  prmreclem5  16891  1arith  16898  2expltfac  17063  mndodconglem  19471  sylow1lem1  19528  gzrngunit  21350  nlmvscnlem1  24574  nrginvrcnlem  24579  iccpnfhmeo  24843  cnheibor  24854  evth  24858  lebnumlem1  24860  ipcnlem1  25145  lmnn  25163  ovolicc2lem2  25419  itg2monolem1  25651  itg2monolem3  25653  dvferm1lem  25888  dvcnvre  25924  dvfsumlem3  25935  dvfsumrlim  25938  plyco0  26097  aaliou2b  26249  pilem2  26362  cosq34lt1  26436  cosordlem  26439  logdivlti  26529  logdivle  26531  logcnlem3  26553  logcnlem4  26554  cxpcn3lem  26657  atanre  26795  atanlogaddlem  26823  atans2  26841  birthdaylem3  26863  cxp2lim  26887  cxploglim2  26889  jensenlem2  26898  harmonicubnd  26920  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamucov  26948  ftalem2  26984  ftalem5  26987  vma1  27076  chtrpcl  27085  ppiltx  27087  fsumfldivdiaglem  27099  chtub  27123  fsumvma2  27125  chpval2  27129  chpchtsum  27130  chpub  27131  bpos1  27194  bposlem1  27195  bposlem2  27196  bposlem6  27200  gausslemma2dlem0c  27269  lgsquadlem1  27291  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chto1ub  27387  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  rplogsumlem2  27396  dchrisumlema  27399  dchrisumlem3  27402  dchrmusumlema  27404  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0lema  27425  mulog2sumlem1  27445  chpdifbndlem1  27464  chpdifbnd  27466  pntrsumo1  27476  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntlemb  27508  pntlemh  27510  pntlemr  27513  pntlem3  27520  pnt2  27524  ostth2lem1  27529  ostth2lem3  27546  ostth2lem4  27547  axsegconlem7  28850  axsegconlem10  28853  axlowdimlem16  28884  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  clwlkclwwlklem2a2  29922  clwwlkext2edg  29985  smatrcl  33786  1smat1  33794  lmdvg  33943  dya2icoseg  34268  eulerpartlems  34351  reprlt  34610  reprinfz1  34613  breprexplemc  34623  hgt750lemd  34639  hgt750lem  34642  hgt750leme  34649  tgoldbachgtde  34651  subfacval3  35176  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem14  36513  knoppndvlem18  36517  poimirlem7  37621  poimirlem24  37638  poimirlem29  37643  mblfinlem2  37652  itg2addnclem  37665  itg2addnclem3  37667  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anc  37695  areacirclem5  37706  lcmineqlem23  42039  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  aks4d1lem1  42050  dvrelog2  42052  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  hashscontpow1  42109  aks6d1c3  42111  2ap1caineq  42133  sticksstones12a  42145  sticksstones22  42156  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  aks5lem8  42189  flt4lem7  42647  3cubeslem1  42672  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pell14qrgapw  42864  pellqrex  42867  pellfundgt1  42871  pellfundex  42874  ltrmxnn0  42938  jm2.24nn  42948  jm2.17c  42951  jm2.24  42952  jm2.23  42985  jm3.1lem1  43006  jm3.1lem2  43007  radcnvrat  44303  dstregt0  45280  monoords  45295  uzubioo  45563  fsumnncl  45570  mullimc  45614  mullimcf  45621  sumnnodd  45628  limcleqr  45642  addlimc  45646  0ellimcdiv  45647  limclner  45649  limsupgtlem  45775  dvdivbd  45921  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  stoweidlem11  46009  stoweidlem24  46022  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem36  46034  stoweidlem42  46040  stoweidlem44  46042  stoweidlem51  46049  stoweidlem59  46057  wallispi  46068  wallispi2lem1  46069  wallispi2  46071  stirlinglem11  46082  dirkertrigeqlem1  46096  dirkeritg  46100  fourierdlem10  46115  fourierdlem11  46116  fourierdlem12  46117  fourierdlem15  46120  fourierdlem19  46124  fourierdlem20  46125  fourierdlem30  46135  fourierdlem32  46137  fourierdlem40  46145  fourierdlem41  46146  fourierdlem44  46149  fourierdlem46  46150  fourierdlem47  46151  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem89  46193  fourierdlem92  46196  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  etransclem4  46236  etransclem23  46255  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem48  46280  ioorrnopnlem  46302  sge0uzfsumgt  46442  sge0seq  46444  iundjiun  46458  carageniuncllem2  46520  hoidmvlelem3  46595  iunhoiioolem  46673  vonioolem1  46678  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  ceilhalfgt1  47330  modm2nep1  47367  modp2nep1  47368  modm1nep2  47369  modm1nem2  47370  modm1p1ne  47371  bgoldbtbndlem2  47807  gpgprismgrusgra  48049  gpg3nbgrvtx0  48067  gpg3kgrtriexlem1  48074  logbpw2m1  48556