Theorem ltletrd 11418

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298

This theorem is referenced by:  lelttrdi  11420  uzwo3  12982  rpgecl  13060  fznatpl1  13614  modabs  13940  seqf1olem1  14078  expgt1  14137  leexp2a  14208  bernneq3  14266  expnbnd  14267  expmulnbnd  14270  digit1  14272  discr1  14274  hashfun  14472  seqcoll2  14500  abssubne0  15351  icodiamlt  15470  reccn2  15629  isercolllem1  15697  isumltss  15880  fprodntriv  15974  efcllem  16109  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  eirrlem  16236  rpnnen2lem11  16256  ruclem10  16271  bitsmod  16469  bitsinv1lem  16474  smuval2  16515  prmreclem5  16953  1arith  16960  2expltfac  17126  mndodconglem  19573  sylow1lem1  19630  gzrngunit  21468  nlmvscnlem1  24722  nrginvrcnlem  24727  iccpnfhmeo  24989  cnheibor  25000  evth  25004  lebnumlem1  25006  ipcnlem1  25292  lmnn  25310  ovolicc2lem2  25566  itg2monolem1  25799  itg2monolem3  25801  dvferm1lem  26036  dvcnvre  26072  dvfsumlem3  26083  dvfsumrlim  26086  plyco0  26245  aaliou2b  26397  pilem2  26510  cosq34lt1  26583  cosordlem  26586  logdivlti  26676  logdivle  26678  logcnlem3  26700  logcnlem4  26701  cxpcn3lem  26804  atanre  26942  atanlogaddlem  26970  atans2  26988  birthdaylem3  27010  cxp2lim  27034  cxploglim2  27036  jensenlem2  27045  harmonicubnd  27067  fsumharmonic  27069  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamucov  27095  ftalem2  27131  ftalem5  27134  vma1  27223  chtrpcl  27232  ppiltx  27234  fsumfldivdiaglem  27246  chtub  27270  fsumvma2  27272  chpval2  27276  chpchtsum  27277  chpub  27278  bpos1  27341  bposlem1  27342  bposlem2  27343  bposlem6  27347  gausslemma2dlem0c  27416  lgsquadlem1  27438  chebbnd1lem1  27527  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chtppilimlem2  27532  chtppilim  27533  chto1ub  27534  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  rplogsumlem2  27543  dchrisumlema  27546  dchrisumlem3  27549  dchrmusumlema  27551  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0lema  27572  mulog2sumlem1  27592  chpdifbndlem1  27611  chpdifbnd  27613  pntrsumo1  27623  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntlemb  27655  pntlemh  27657  pntlemr  27660  pntlem3  27667  pnt2  27671  ostth2lem1  27676  ostth2lem3  27693  ostth2lem4  27694  axsegconlem7  28952  axsegconlem10  28955  axlowdimlem16  28986  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  clwlkclwwlklem2a2  30021  clwwlkext2edg  30084  smatrcl  33756  1smat1  33764  lmdvg  33913  dya2icoseg  34258  eulerpartlems  34341  reprlt  34612  reprinfz1  34615  breprexplemc  34625  hgt750lemd  34641  hgt750lem  34644  hgt750leme  34651  tgoldbachgtde  34653  subfacval3  35173  knoppndvlem1  36494  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem14  36507  knoppndvlem18  36511  poimirlem7  37613  poimirlem24  37630  poimirlem29  37635  mblfinlem2  37644  itg2addnclem  37657  itg2addnclem3  37659  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anc  37687  areacirclem5  37698  lcmineqlem23  42032  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  aks4d1lem1  42043  dvrelog2  42045  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  hashscontpow1  42102  aks6d1c3  42104  2ap1caineq  42126  sticksstones12a  42138  sticksstones22  42149  aks6d1c7lem1  42161  aks6d1c7lem2  42162  aks6d1c7  42165  aks5lem6  42173  aks5lem8  42182  metakunt6  42191  metakunt11  42196  metakunt27  42212  metakunt28  42213  flt4lem7  42645  3cubeslem1  42671  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pell14qrgapw  42863  pellqrex  42866  pellfundgt1  42870  pellfundex  42873  ltrmxnn0  42937  jm2.24nn  42947  jm2.17c  42950  jm2.24  42951  jm2.23  42984  jm3.1lem1  43005  jm3.1lem2  43006  radcnvrat  44309  dstregt0  45231  monoords  45247  uzubioo  45519  fsumnncl  45527  mullimc  45571  mullimcf  45578  sumnnodd  45585  limcleqr  45599  addlimc  45603  0ellimcdiv  45604  limclner  45606  limsupgtlem  45732  dvdivbd  45878  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  iblspltprt  45928  itgspltprt  45934  stoweidlem11  45966  stoweidlem24  45979  stoweidlem25  45980  stoweidlem26  45981  stoweidlem34  45989  stoweidlem36  45991  stoweidlem42  45997  stoweidlem44  45999  stoweidlem51  46006  stoweidlem59  46014  wallispi  46025  wallispi2lem1  46026  wallispi2  46028  stirlinglem11  46039  dirkertrigeqlem1  46053  dirkeritg  46057  fourierdlem10  46072  fourierdlem11  46073  fourierdlem12  46074  fourierdlem15  46077  fourierdlem19  46081  fourierdlem20  46082  fourierdlem30  46092  fourierdlem32  46094  fourierdlem40  46102  fourierdlem41  46103  fourierdlem44  46106  fourierdlem46  46107  fourierdlem47  46108  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem89  46150  fourierdlem92  46153  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  etransclem4  46193  etransclem23  46212  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem41  46230  etransclem48  46237  ioorrnopnlem  46259  sge0uzfsumgt  46399  sge0seq  46401  iundjiun  46415  carageniuncllem2  46477  hoidmvlelem3  46552  iunhoiioolem  46630  vonioolem1  46635  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  bgoldbtbndlem2  47730  gpg3nbgrvtx0  47966  logbpw2m1  48416