Theorem ltletrd 11310

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 11242	. . 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 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118  ax-pre-lttrn 11119

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 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  lelttrdi  11312  uzwo3  12878  rpgecl  12957  fznatpl1  13515  modabs  13842  seqf1olem1  13982  expgt1  14041  leexp2a  14113  bernneq3  14172  expnbnd  14173  expmulnbnd  14176  digit1  14178  discr1  14180  hashfun  14378  seqcoll2  14406  abssubne0  15259  icodiamlt  15380  reccn2  15539  isercolllem1  15607  isumltss  15790  fprodntriv  15884  efcllem  16019  sin01bnd  16129  cos01bnd  16130  sin01gt0  16134  eirrlem  16148  rpnnen2lem11  16168  ruclem10  16183  bitsmod  16382  bitsinv1lem  16387  smuval2  16428  prmreclem5  16867  1arith  16874  2expltfac  17039  mndodconglem  19447  sylow1lem1  19504  gzrngunit  21326  nlmvscnlem1  24550  nrginvrcnlem  24555  iccpnfhmeo  24819  cnheibor  24830  evth  24834  lebnumlem1  24836  ipcnlem1  25121  lmnn  25139  ovolicc2lem2  25395  itg2monolem1  25627  itg2monolem3  25629  dvferm1lem  25864  dvcnvre  25900  dvfsumlem3  25911  dvfsumrlim  25914  plyco0  26073  aaliou2b  26225  pilem2  26338  cosq34lt1  26412  cosordlem  26415  logdivlti  26505  logdivle  26507  logcnlem3  26529  logcnlem4  26530  cxpcn3lem  26633  atanre  26771  atanlogaddlem  26799  atans2  26817  birthdaylem3  26839  cxp2lim  26863  cxploglim2  26865  jensenlem2  26874  harmonicubnd  26896  fsumharmonic  26898  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamucov  26924  ftalem2  26960  ftalem5  26963  vma1  27052  chtrpcl  27061  ppiltx  27063  fsumfldivdiaglem  27075  chtub  27099  fsumvma2  27101  chpval2  27105  chpchtsum  27106  chpub  27107  bpos1  27170  bposlem1  27171  bposlem2  27172  bposlem6  27176  gausslemma2dlem0c  27245  lgsquadlem1  27267  chebbnd1lem1  27356  chebbnd1lem2  27357  chebbnd1lem3  27358  chebbnd1  27359  chtppilimlem1  27360  chtppilimlem2  27361  chtppilim  27362  chto1ub  27363  chebbnd2  27364  chto1lb  27365  chpchtlim  27366  chpo1ub  27367  rplogsumlem2  27372  dchrisumlema  27375  dchrisumlem3  27378  dchrmusumlema  27380  dchrvmasumlem2  27385  dchrvmasumiflem1  27388  dchrisum0lema  27401  mulog2sumlem1  27421  chpdifbndlem1  27440  chpdifbnd  27442  pntrsumo1  27452  pntpbnd1  27473  pntpbnd2  27474  pntibndlem2  27478  pntlemb  27484  pntlemh  27486  pntlemr  27489  pntlem3  27496  pnt2  27500  ostth2lem1  27505  ostth2lem3  27522  ostth2lem4  27523  axsegconlem7  28826  axsegconlem10  28829  axlowdimlem16  28860  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  clwlkclwwlklem2a2  29895  clwwlkext2edg  29958  smatrcl  33759  1smat1  33767  lmdvg  33916  dya2icoseg  34241  eulerpartlems  34324  reprlt  34583  reprinfz1  34586  breprexplemc  34596  hgt750lemd  34612  hgt750lem  34615  hgt750leme  34622  tgoldbachgtde  34624  subfacval3  35149  knoppndvlem1  36473  knoppndvlem2  36474  knoppndvlem7  36479  knoppndvlem14  36486  knoppndvlem18  36490  poimirlem7  37594  poimirlem24  37611  poimirlem29  37616  mblfinlem2  37625  itg2addnclem  37638  itg2addnclem3  37640  ftc1anclem5  37664  ftc1anclem7  37666  ftc1anc  37668  areacirclem5  37679  lcmineqlem23  42012  3lexlogpow5ineq2  42016  3lexlogpow5ineq4  42017  3lexlogpow5ineq3  42018  aks4d1lem1  42023  dvrelog2  42025  aks4d1p1p3  42030  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p2  42038  aks4d1p3  42039  aks4d1p5  42041  aks4d1p6  42042  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8d2  42046  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  hashscontpow1  42082  aks6d1c3  42084  2ap1caineq  42106  sticksstones12a  42118  sticksstones22  42129  aks6d1c7lem1  42141  aks6d1c7lem2  42142  aks6d1c7  42145  aks5lem6  42153  aks5lem8  42162  flt4lem7  42620  3cubeslem1  42645  irrapxlem4  42786  irrapxlem5  42787  pellexlem2  42791  pell14qrgapw  42837  pellqrex  42840  pellfundgt1  42844  pellfundex  42847  ltrmxnn0  42911  jm2.24nn  42921  jm2.17c  42924  jm2.24  42925  jm2.23  42958  jm3.1lem1  42979  jm3.1lem2  42980  radcnvrat  44276  dstregt0  45253  monoords  45268  uzubioo  45536  fsumnncl  45543  mullimc  45587  mullimcf  45594  sumnnodd  45601  limcleqr  45615  addlimc  45619  0ellimcdiv  45620  limclner  45622  limsupgtlem  45748  dvdivbd  45894  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnmul  45914  iblspltprt  45944  itgspltprt  45950  stoweidlem11  45982  stoweidlem24  45995  stoweidlem25  45996  stoweidlem26  45997  stoweidlem34  46005  stoweidlem36  46007  stoweidlem42  46013  stoweidlem44  46015  stoweidlem51  46022  stoweidlem59  46030  wallispi  46041  wallispi2lem1  46042  wallispi2  46044  stirlinglem11  46055  dirkertrigeqlem1  46069  dirkeritg  46073  fourierdlem10  46088  fourierdlem11  46089  fourierdlem12  46090  fourierdlem15  46093  fourierdlem19  46097  fourierdlem20  46098  fourierdlem30  46108  fourierdlem32  46110  fourierdlem40  46118  fourierdlem41  46119  fourierdlem44  46122  fourierdlem46  46123  fourierdlem47  46124  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem78  46155  fourierdlem79  46156  fourierdlem89  46166  fourierdlem92  46169  fourierdlem103  46180  fourierdlem104  46181  fouriersw  46202  etransclem4  46209  etransclem23  46228  etransclem31  46236  etransclem32  46237  etransclem35  46240  etransclem41  46246  etransclem48  46253  ioorrnopnlem  46275  sge0uzfsumgt  46415  sge0seq  46417  iundjiun  46431  carageniuncllem2  46493  hoidmvlelem3  46568  iunhoiioolem  46646  vonioolem1  46651  smfmullem1  46762  smfmullem2  46763  smfmullem3  46764  ceilhalfgt1  47303  modm2nep1  47340  modp2nep1  47341  modm1nep2  47342  modm1nem2  47343  modm1p1ne  47344  bgoldbtbndlem2  47780  gpgprismgrusgra  48022  gpg3nbgrvtx0  48040  gpg3kgrtriexlem1  48047  logbpw2m1  48529