Theorem ltletrd 11370

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5147  ℝcr 11105   < clt 11244   ≤ cle 11245

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250

This theorem is referenced by:  lelttrdi  11372  uzwo3  12923  rpgecl  12998  fznatpl1  13551  modabs  13865  seqf1olem1  14003  expgt1  14062  leexp2a  14133  bernneq3  14190  expnbnd  14191  expmulnbnd  14194  digit1  14196  discr1  14198  hashfun  14393  seqcoll2  14422  abssubne0  15259  icodiamlt  15378  reccn2  15537  isercolllem1  15607  isumltss  15790  fprodntriv  15882  efcllem  16017  sin01bnd  16124  cos01bnd  16125  sin01gt0  16129  eirrlem  16143  rpnnen2lem11  16163  ruclem10  16178  bitsmod  16373  bitsinv1lem  16378  smuval2  16419  prmreclem5  16849  1arith  16856  2expltfac  17022  mndodconglem  19403  sylow1lem1  19460  gzrngunit  21003  nlmvscnlem1  24194  nrginvrcnlem  24199  iccpnfhmeo  24452  cnheibor  24462  evth  24466  lebnumlem1  24468  ipcnlem1  24753  lmnn  24771  ovolicc2lem2  25026  itg2monolem1  25259  itg2monolem3  25261  dvferm1lem  25492  dvcnvre  25527  dvfsumlem3  25536  dvfsumrlim  25539  plyco0  25697  aaliou2b  25845  pilem2  25955  cosq34lt1  26027  cosordlem  26030  logdivlti  26119  logdivle  26121  logcnlem3  26143  logcnlem4  26144  cxpcn3lem  26244  atanre  26379  atanlogaddlem  26407  atans2  26425  birthdaylem3  26447  cxp2lim  26470  cxploglim2  26472  jensenlem2  26481  harmonicubnd  26503  fsumharmonic  26505  lgamgulmlem2  26523  lgamgulmlem3  26524  lgamucov  26531  ftalem2  26567  ftalem5  26570  vma1  26659  chtrpcl  26668  ppiltx  26670  fsumfldivdiaglem  26682  chtub  26704  fsumvma2  26706  chpval2  26710  chpchtsum  26711  chpub  26712  bpos1  26775  bposlem1  26776  bposlem2  26777  bposlem6  26781  gausslemma2dlem0c  26850  lgsquadlem1  26872  chebbnd1lem1  26961  chebbnd1lem2  26962  chebbnd1lem3  26963  chebbnd1  26964  chtppilimlem1  26965  chtppilimlem2  26966  chtppilim  26967  chto1ub  26968  chebbnd2  26969  chto1lb  26970  chpchtlim  26971  chpo1ub  26972  rplogsumlem2  26977  dchrisumlema  26980  dchrisumlem3  26983  dchrmusumlema  26985  dchrvmasumlem2  26990  dchrvmasumiflem1  26993  dchrisum0lema  27006  mulog2sumlem1  27026  chpdifbndlem1  27045  chpdifbnd  27047  pntrsumo1  27057  pntpbnd1  27078  pntpbnd2  27079  pntibndlem2  27083  pntlemb  27089  pntlemh  27091  pntlemr  27094  pntlem3  27101  pnt2  27105  ostth2lem1  27110  ostth2lem3  27127  ostth2lem4  27128  axsegconlem7  28170  axsegconlem10  28173  axlowdimlem16  28204  axcontlem2  28212  axcontlem4  28214  axcontlem7  28217  clwlkclwwlklem2a2  29235  clwwlkext2edg  29298  smatrcl  32764  1smat1  32772  lmdvg  32921  dya2icoseg  33264  eulerpartlems  33347  reprlt  33619  reprinfz1  33622  breprexplemc  33632  hgt750lemd  33648  hgt750lem  33651  hgt750leme  33658  tgoldbachgtde  33660  subfacval3  34168  knoppndvlem1  35376  knoppndvlem2  35377  knoppndvlem7  35382  knoppndvlem14  35389  knoppndvlem18  35393  poimirlem7  36483  poimirlem24  36500  poimirlem29  36505  mblfinlem2  36514  itg2addnclem  36527  itg2addnclem3  36529  ftc1anclem5  36553  ftc1anclem7  36555  ftc1anc  36557  areacirclem5  36568  lcmineqlem23  40904  3lexlogpow5ineq2  40908  3lexlogpow5ineq4  40909  3lexlogpow5ineq3  40910  aks4d1lem1  40915  dvrelog2  40917  aks4d1p1p3  40922  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p1p6  40926  aks4d1p1p7  40927  aks4d1p1p5  40928  aks4d1p1  40929  aks4d1p2  40930  aks4d1p3  40931  aks4d1p5  40933  aks4d1p6  40934  aks4d1p7d1  40935  aks4d1p7  40936  aks4d1p8d2  40938  aks4d1p8  40940  aks4d1p9  40941  2ap1caineq  40949  sticksstones12a  40961  sticksstones22  40972  metakunt6  40978  metakunt11  40983  metakunt27  40999  metakunt28  41000  flt4lem7  41397  3cubeslem1  41407  irrapxlem4  41548  irrapxlem5  41549  pellexlem2  41553  pell14qrgapw  41599  pellqrex  41602  pellfundgt1  41606  pellfundex  41609  ltrmxnn0  41673  jm2.24nn  41683  jm2.17c  41686  jm2.24  41687  jm2.23  41720  jm3.1lem1  41741  jm3.1lem2  41742  radcnvrat  43058  dstregt0  43977  monoords  43993  uzubioo  44266  fsumnncl  44274  mullimc  44318  mullimcf  44325  sumnnodd  44332  limcleqr  44346  addlimc  44350  0ellimcdiv  44351  limclner  44353  limsupgtlem  44479  dvdivbd  44625  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  dvnmul  44645  iblspltprt  44675  itgspltprt  44681  stoweidlem11  44713  stoweidlem24  44726  stoweidlem25  44727  stoweidlem26  44728  stoweidlem34  44736  stoweidlem36  44738  stoweidlem42  44744  stoweidlem44  44746  stoweidlem51  44753  stoweidlem59  44761  wallispi  44772  wallispi2lem1  44773  wallispi2  44775  stirlinglem11  44786  dirkertrigeqlem1  44800  dirkeritg  44804  fourierdlem10  44819  fourierdlem11  44820  fourierdlem12  44821  fourierdlem15  44824  fourierdlem19  44828  fourierdlem20  44829  fourierdlem30  44839  fourierdlem32  44841  fourierdlem40  44849  fourierdlem41  44850  fourierdlem44  44853  fourierdlem46  44854  fourierdlem47  44855  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem63  44871  fourierdlem64  44872  fourierdlem65  44873  fourierdlem74  44882  fourierdlem75  44883  fourierdlem76  44884  fourierdlem78  44886  fourierdlem79  44887  fourierdlem89  44897  fourierdlem92  44900  fourierdlem103  44911  fourierdlem104  44912  fouriersw  44933  etransclem4  44940  etransclem23  44959  etransclem31  44967  etransclem32  44968  etransclem35  44971  etransclem41  44977  etransclem48  44984  ioorrnopnlem  45006  sge0uzfsumgt  45146  sge0seq  45148  iundjiun  45162  carageniuncllem2  45224  hoidmvlelem3  45299  iunhoiioolem  45377  vonioolem1  45382  smfmullem1  45493  smfmullem2  45494  smfmullem3  45495  bgoldbtbndlem2  46460  logbpw2m1  47206