Theorem ltletrd 11144

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879   < clt 11018   ≤ cle 11019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-pre-lttri 10954  ax-pre-lttrn 10955

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024

This theorem is referenced by:  lelttrdi  11146  uzwo3  12692  rpgecl  12767  fznatpl1  13319  modabs  13633  seqf1olem1  13771  expgt1  13830  leexp2a  13899  bernneq3  13955  expnbnd  13956  expmulnbnd  13959  digit1  13961  discr1  13963  hashfun  14161  seqcoll2  14188  abssubne0  15037  icodiamlt  15156  reccn2  15315  isercolllem1  15385  isumltss  15569  fprodntriv  15661  efcllem  15796  sin01bnd  15903  cos01bnd  15904  sin01gt0  15908  eirrlem  15922  rpnnen2lem11  15942  ruclem10  15957  bitsmod  16152  bitsinv1lem  16157  smuval2  16198  prmreclem5  16630  1arith  16637  2expltfac  16803  mndodconglem  19158  sylow1lem1  19212  gzrngunit  20673  nlmvscnlem1  23859  nrginvrcnlem  23864  iccpnfhmeo  24117  cnheibor  24127  evth  24131  lebnumlem1  24133  ipcnlem1  24418  lmnn  24436  ovolicc2lem2  24691  itg2monolem1  24924  itg2monolem3  24926  dvferm1lem  25157  dvcnvre  25192  dvfsumlem3  25201  dvfsumrlim  25204  plyco0  25362  aaliou2b  25510  pilem2  25620  cosq34lt1  25692  cosordlem  25695  logdivlti  25784  logdivle  25786  logcnlem3  25808  logcnlem4  25809  cxpcn3lem  25909  atanre  26044  atanlogaddlem  26072  atans2  26090  birthdaylem3  26112  cxp2lim  26135  cxploglim2  26137  jensenlem2  26146  harmonicubnd  26168  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamucov  26196  ftalem2  26232  ftalem5  26235  vma1  26324  chtrpcl  26333  ppiltx  26335  fsumfldivdiaglem  26347  chtub  26369  fsumvma2  26371  chpval2  26375  chpchtsum  26376  chpub  26377  bpos1  26440  bposlem1  26441  bposlem2  26442  bposlem6  26446  gausslemma2dlem0c  26515  lgsquadlem1  26537  chebbnd1lem1  26626  chebbnd1lem2  26627  chebbnd1lem3  26628  chebbnd1  26629  chtppilimlem1  26630  chtppilimlem2  26631  chtppilim  26632  chto1ub  26633  chebbnd2  26634  chto1lb  26635  chpchtlim  26636  chpo1ub  26637  rplogsumlem2  26642  dchrisumlema  26645  dchrisumlem3  26648  dchrmusumlema  26650  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrisum0lema  26671  mulog2sumlem1  26691  chpdifbndlem1  26710  chpdifbnd  26712  pntrsumo1  26722  pntpbnd1  26743  pntpbnd2  26744  pntibndlem2  26748  pntlemb  26754  pntlemh  26756  pntlemr  26759  pntlem3  26766  pnt2  26770  ostth2lem1  26775  ostth2lem3  26792  ostth2lem4  26793  axsegconlem7  27300  axsegconlem10  27303  axlowdimlem16  27334  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  clwlkclwwlklem2a2  28366  clwwlkext2edg  28429  smatrcl  31755  1smat1  31763  lmdvg  31912  dya2icoseg  32253  eulerpartlems  32336  reprlt  32608  reprinfz1  32611  breprexplemc  32621  hgt750lemd  32637  hgt750lem  32640  hgt750leme  32647  tgoldbachgtde  32649  subfacval3  33160  knoppndvlem1  34701  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem14  34714  knoppndvlem18  34718  poimirlem7  35793  poimirlem24  35810  poimirlem29  35815  mblfinlem2  35824  itg2addnclem  35837  itg2addnclem3  35839  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anc  35867  areacirclem5  35878  lcmineqlem23  40066  3lexlogpow5ineq2  40070  3lexlogpow5ineq4  40071  3lexlogpow5ineq3  40072  aks4d1lem1  40077  dvrelog2  40079  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  2ap1caineq  40108  sticksstones12a  40120  sticksstones22  40131  metakunt6  40137  metakunt11  40142  metakunt27  40158  metakunt28  40159  flt4lem7  40503  3cubeslem1  40513  irrapxlem4  40654  irrapxlem5  40655  pellexlem2  40659  pell14qrgapw  40705  pellqrex  40708  pellfundgt1  40712  pellfundex  40715  ltrmxnn0  40778  jm2.24nn  40788  jm2.17c  40791  jm2.24  40792  jm2.23  40825  jm3.1lem1  40846  jm3.1lem2  40847  radcnvrat  41939  dstregt0  42827  monoords  42843  uzubioo  43112  fsumnncl  43120  mullimc  43164  mullimcf  43171  sumnnodd  43178  limcleqr  43192  addlimc  43196  0ellimcdiv  43197  limclner  43199  limsupgtlem  43325  dvdivbd  43471  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  iblspltprt  43521  itgspltprt  43527  stoweidlem11  43559  stoweidlem24  43572  stoweidlem25  43573  stoweidlem26  43574  stoweidlem34  43582  stoweidlem36  43584  stoweidlem42  43590  stoweidlem44  43592  stoweidlem51  43599  stoweidlem59  43607  wallispi  43618  wallispi2lem1  43619  wallispi2  43621  stirlinglem11  43632  dirkertrigeqlem1  43646  dirkeritg  43650  fourierdlem10  43665  fourierdlem11  43666  fourierdlem12  43667  fourierdlem15  43670  fourierdlem19  43674  fourierdlem20  43675  fourierdlem30  43685  fourierdlem32  43687  fourierdlem40  43695  fourierdlem41  43696  fourierdlem44  43699  fourierdlem46  43700  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem78  43732  fourierdlem79  43733  fourierdlem89  43743  fourierdlem92  43746  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  etransclem4  43786  etransclem23  43805  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem48  43830  ioorrnopnlem  43852  sge0uzfsumgt  43989  sge0seq  43991  iundjiun  44005  carageniuncllem2  44067  hoidmvlelem3  44142  iunhoiioolem  44220  vonioolem1  44225  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  bgoldbtbndlem2  45269  logbpw2m1  45924