Theorem ltletrd 11372

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098   class class class wbr 5139  ℝcr 11106   < clt 11246   ≤ cle 11247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-pre-lttri 11181  ax-pre-lttrn 11182

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252

This theorem is referenced by:  lelttrdi  11374  uzwo3  12925  rpgecl  13000  fznatpl1  13553  modabs  13867  seqf1olem1  14005  expgt1  14064  leexp2a  14135  bernneq3  14192  expnbnd  14193  expmulnbnd  14196  digit1  14198  discr1  14200  hashfun  14395  seqcoll2  14424  abssubne0  15261  icodiamlt  15380  reccn2  15539  isercolllem1  15609  isumltss  15792  fprodntriv  15884  efcllem  16019  sin01bnd  16127  cos01bnd  16128  sin01gt0  16132  eirrlem  16146  rpnnen2lem11  16166  ruclem10  16181  bitsmod  16376  bitsinv1lem  16381  smuval2  16422  prmreclem5  16854  1arith  16861  2expltfac  17027  mndodconglem  19453  sylow1lem1  19510  gzrngunit  21297  nlmvscnlem1  24527  nrginvrcnlem  24532  iccpnfhmeo  24794  cnheibor  24805  evth  24809  lebnumlem1  24811  ipcnlem1  25097  lmnn  25115  ovolicc2lem2  25371  itg2monolem1  25604  itg2monolem3  25606  dvferm1lem  25840  dvcnvre  25876  dvfsumlem3  25887  dvfsumrlim  25890  plyco0  26048  aaliou2b  26197  pilem2  26308  cosq34lt1  26380  cosordlem  26383  logdivlti  26473  logdivle  26475  logcnlem3  26497  logcnlem4  26498  cxpcn3lem  26601  atanre  26736  atanlogaddlem  26764  atans2  26782  birthdaylem3  26804  cxp2lim  26828  cxploglim2  26830  jensenlem2  26839  harmonicubnd  26861  fsumharmonic  26863  lgamgulmlem2  26881  lgamgulmlem3  26882  lgamucov  26889  ftalem2  26925  ftalem5  26928  vma1  27017  chtrpcl  27026  ppiltx  27028  fsumfldivdiaglem  27040  chtub  27064  fsumvma2  27066  chpval2  27070  chpchtsum  27071  chpub  27072  bpos1  27135  bposlem1  27136  bposlem2  27137  bposlem6  27141  gausslemma2dlem0c  27210  lgsquadlem1  27232  chebbnd1lem1  27321  chebbnd1lem2  27322  chebbnd1lem3  27323  chebbnd1  27324  chtppilimlem1  27325  chtppilimlem2  27326  chtppilim  27327  chto1ub  27328  chebbnd2  27329  chto1lb  27330  chpchtlim  27331  chpo1ub  27332  rplogsumlem2  27337  dchrisumlema  27340  dchrisumlem3  27343  dchrmusumlema  27345  dchrvmasumlem2  27350  dchrvmasumiflem1  27353  dchrisum0lema  27366  mulog2sumlem1  27386  chpdifbndlem1  27405  chpdifbnd  27407  pntrsumo1  27417  pntpbnd1  27438  pntpbnd2  27439  pntibndlem2  27443  pntlemb  27449  pntlemh  27451  pntlemr  27454  pntlem3  27461  pnt2  27465  ostth2lem1  27470  ostth2lem3  27487  ostth2lem4  27488  axsegconlem7  28653  axsegconlem10  28656  axlowdimlem16  28687  axcontlem2  28695  axcontlem4  28697  axcontlem7  28700  clwlkclwwlklem2a2  29718  clwwlkext2edg  29781  smatrcl  33268  1smat1  33276  lmdvg  33425  dya2icoseg  33768  eulerpartlems  33851  reprlt  34122  reprinfz1  34125  breprexplemc  34135  hgt750lemd  34151  hgt750lem  34154  hgt750leme  34161  tgoldbachgtde  34163  subfacval3  34671  knoppndvlem1  35879  knoppndvlem2  35880  knoppndvlem7  35885  knoppndvlem14  35892  knoppndvlem18  35896  poimirlem7  36989  poimirlem24  37006  poimirlem29  37011  mblfinlem2  37020  itg2addnclem  37033  itg2addnclem3  37035  ftc1anclem5  37059  ftc1anclem7  37061  ftc1anc  37063  areacirclem5  37074  lcmineqlem23  41413  3lexlogpow5ineq2  41417  3lexlogpow5ineq4  41418  3lexlogpow5ineq3  41419  aks4d1lem1  41424  dvrelog2  41426  aks4d1p1p3  41431  aks4d1p1p2  41432  aks4d1p1p4  41433  aks4d1p1p6  41435  aks4d1p1p7  41436  aks4d1p1p5  41437  aks4d1p1  41438  aks4d1p2  41439  aks4d1p3  41440  aks4d1p5  41442  aks4d1p6  41443  aks4d1p7d1  41444  aks4d1p7  41445  aks4d1p8d2  41447  aks4d1p8  41449  aks4d1p9  41450  2ap1caineq  41458  sticksstones12a  41470  sticksstones22  41481  metakunt6  41487  metakunt11  41492  metakunt27  41508  metakunt28  41509  flt4lem7  41915  3cubeslem1  41936  irrapxlem4  42077  irrapxlem5  42078  pellexlem2  42082  pell14qrgapw  42128  pellqrex  42131  pellfundgt1  42135  pellfundex  42138  ltrmxnn0  42202  jm2.24nn  42212  jm2.17c  42215  jm2.24  42216  jm2.23  42249  jm3.1lem1  42270  jm3.1lem2  42271  radcnvrat  43587  dstregt0  44501  monoords  44517  uzubioo  44790  fsumnncl  44798  mullimc  44842  mullimcf  44849  sumnnodd  44856  limcleqr  44870  addlimc  44874  0ellimcdiv  44875  limclner  44877  limsupgtlem  45003  dvdivbd  45149  ioodvbdlimc1lem1  45157  ioodvbdlimc1lem2  45158  ioodvbdlimc2lem  45160  dvnmul  45169  iblspltprt  45199  itgspltprt  45205  stoweidlem11  45237  stoweidlem24  45250  stoweidlem25  45251  stoweidlem26  45252  stoweidlem34  45260  stoweidlem36  45262  stoweidlem42  45268  stoweidlem44  45270  stoweidlem51  45277  stoweidlem59  45285  wallispi  45296  wallispi2lem1  45297  wallispi2  45299  stirlinglem11  45310  dirkertrigeqlem1  45324  dirkeritg  45328  fourierdlem10  45343  fourierdlem11  45344  fourierdlem12  45345  fourierdlem15  45348  fourierdlem19  45352  fourierdlem20  45353  fourierdlem30  45363  fourierdlem32  45365  fourierdlem40  45373  fourierdlem41  45374  fourierdlem44  45377  fourierdlem46  45378  fourierdlem47  45379  fourierdlem48  45380  fourierdlem49  45381  fourierdlem50  45382  fourierdlem63  45395  fourierdlem64  45396  fourierdlem65  45397  fourierdlem74  45406  fourierdlem75  45407  fourierdlem76  45408  fourierdlem78  45410  fourierdlem79  45411  fourierdlem89  45421  fourierdlem92  45424  fourierdlem103  45435  fourierdlem104  45436  fouriersw  45457  etransclem4  45464  etransclem23  45483  etransclem31  45491  etransclem32  45492  etransclem35  45495  etransclem41  45501  etransclem48  45508  ioorrnopnlem  45530  sge0uzfsumgt  45670  sge0seq  45672  iundjiun  45686  carageniuncllem2  45748  hoidmvlelem3  45823  iunhoiioolem  45901  vonioolem1  45906  smfmullem1  46017  smfmullem2  46018  smfmullem3  46019  bgoldbtbndlem2  46984  logbpw2m1  47466