Theorem ltletrd 11291

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-pre-lttri 11098  ax-pre-lttrn 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170

This theorem is referenced by:  lelttrdi  11293  uzwo3  12854  rpgecl  12933  fznatpl1  13492  modabs  13822  seqf1olem1  13962  expgt1  14021  leexp2a  14093  bernneq3  14152  expnbnd  14153  expmulnbnd  14156  digit1  14158  discr1  14160  hashfun  14358  seqcoll2  14386  abssubne0  15238  icodiamlt  15359  reccn2  15518  isercolllem1  15586  isumltss  15769  fprodntriv  15863  efcllem  15998  sin01bnd  16108  cos01bnd  16109  sin01gt0  16113  eirrlem  16127  rpnnen2lem11  16147  ruclem10  16162  bitsmod  16361  bitsinv1lem  16366  smuval2  16407  prmreclem5  16846  1arith  16853  2expltfac  17018  mndodconglem  19468  sylow1lem1  19525  gzrngunit  21386  nlmvscnlem1  24628  nrginvrcnlem  24633  iccpnfhmeo  24897  cnheibor  24908  evth  24912  lebnumlem1  24914  ipcnlem1  25199  lmnn  25217  ovolicc2lem2  25473  itg2monolem1  25705  itg2monolem3  25707  dvferm1lem  25942  dvcnvre  25978  dvfsumlem3  25989  dvfsumrlim  25992  plyco0  26151  aaliou2b  26303  pilem2  26416  cosq34lt1  26490  cosordlem  26493  logdivlti  26583  logdivle  26585  logcnlem3  26607  logcnlem4  26608  cxpcn3lem  26711  atanre  26849  atanlogaddlem  26877  atans2  26895  birthdaylem3  26917  cxp2lim  26941  cxploglim2  26943  jensenlem2  26952  harmonicubnd  26974  fsumharmonic  26976  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamucov  27002  ftalem2  27038  ftalem5  27041  vma1  27130  chtrpcl  27139  ppiltx  27141  fsumfldivdiaglem  27153  chtub  27177  fsumvma2  27179  chpval2  27183  chpchtsum  27184  chpub  27185  bpos1  27248  bposlem1  27249  bposlem2  27250  bposlem6  27254  gausslemma2dlem0c  27323  lgsquadlem1  27345  chebbnd1lem1  27434  chebbnd1lem2  27435  chebbnd1lem3  27436  chebbnd1  27437  chtppilimlem1  27438  chtppilimlem2  27439  chtppilim  27440  chto1ub  27441  chebbnd2  27442  chto1lb  27443  chpchtlim  27444  chpo1ub  27445  rplogsumlem2  27450  dchrisumlema  27453  dchrisumlem3  27456  dchrmusumlema  27458  dchrvmasumlem2  27463  dchrvmasumiflem1  27466  dchrisum0lema  27479  mulog2sumlem1  27499  chpdifbndlem1  27518  chpdifbnd  27520  pntrsumo1  27530  pntpbnd1  27551  pntpbnd2  27552  pntibndlem2  27556  pntlemb  27562  pntlemh  27564  pntlemr  27567  pntlem3  27574  pnt2  27578  ostth2lem1  27583  ostth2lem3  27600  ostth2lem4  27601  axsegconlem7  28945  axsegconlem10  28948  axlowdimlem16  28979  axcontlem2  28987  axcontlem4  28989  axcontlem7  28992  clwlkclwwlklem2a2  30017  clwwlkext2edg  30080  smatrcl  33902  1smat1  33910  lmdvg  34059  dya2icoseg  34383  eulerpartlems  34466  reprlt  34725  reprinfz1  34728  breprexplemc  34738  hgt750lemd  34754  hgt750lem  34757  hgt750leme  34764  tgoldbachgtde  34766  subfacval3  35332  knoppndvlem1  36655  knoppndvlem2  36656  knoppndvlem7  36661  knoppndvlem14  36668  knoppndvlem18  36672  poimirlem7  37767  poimirlem24  37784  poimirlem29  37789  mblfinlem2  37798  itg2addnclem  37811  itg2addnclem3  37813  ftc1anclem5  37837  ftc1anclem7  37839  ftc1anc  37841  areacirclem5  37852  lcmineqlem23  42244  3lexlogpow5ineq2  42248  3lexlogpow5ineq4  42249  3lexlogpow5ineq3  42250  aks4d1lem1  42255  dvrelog2  42257  aks4d1p1p3  42262  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p2  42270  aks4d1p3  42271  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8d2  42278  aks4d1p8  42280  aks4d1p9  42281  posbezout  42293  hashscontpow1  42314  aks6d1c3  42316  2ap1caineq  42338  sticksstones12a  42350  sticksstones22  42361  aks6d1c7lem1  42373  aks6d1c7lem2  42374  aks6d1c7  42377  aks5lem6  42385  aks5lem8  42394  flt4lem7  42844  3cubeslem1  42868  irrapxlem4  43009  irrapxlem5  43010  pellexlem2  43014  pell14qrgapw  43060  pellqrex  43063  pellfundgt1  43067  pellfundex  43070  ltrmxnn0  43133  jm2.24nn  43143  jm2.17c  43146  jm2.24  43147  jm2.23  43180  jm3.1lem1  43201  jm3.1lem2  43202  radcnvrat  44497  dstregt0  45472  monoords  45487  uzubioo  45753  fsumnncl  45760  mullimc  45804  mullimcf  45811  sumnnodd  45818  limcleqr  45830  addlimc  45834  0ellimcdiv  45835  limclner  45837  limsupgtlem  45963  dvdivbd  46109  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  iblspltprt  46159  itgspltprt  46165  stoweidlem11  46197  stoweidlem24  46210  stoweidlem25  46211  stoweidlem26  46212  stoweidlem34  46220  stoweidlem36  46222  stoweidlem42  46228  stoweidlem44  46230  stoweidlem51  46237  stoweidlem59  46245  wallispi  46256  wallispi2lem1  46257  wallispi2  46259  stirlinglem11  46270  dirkertrigeqlem1  46284  dirkeritg  46288  fourierdlem10  46303  fourierdlem11  46304  fourierdlem12  46305  fourierdlem15  46308  fourierdlem19  46312  fourierdlem20  46313  fourierdlem30  46323  fourierdlem32  46325  fourierdlem40  46333  fourierdlem41  46334  fourierdlem44  46337  fourierdlem46  46338  fourierdlem47  46339  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem79  46371  fourierdlem89  46381  fourierdlem92  46384  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  etransclem4  46424  etransclem23  46443  etransclem31  46451  etransclem32  46452  etransclem35  46455  etransclem41  46461  etransclem48  46468  ioorrnopnlem  46490  sge0uzfsumgt  46630  sge0seq  46632  iundjiun  46646  carageniuncllem2  46708  hoidmvlelem3  46783  iunhoiioolem  46861  vonioolem1  46866  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  ceilhalfgt1  47517  modm2nep1  47554  modp2nep1  47555  modm1nep2  47556  modm1nem2  47557  modm1p1ne  47558  bgoldbtbndlem2  47994  gpgprismgrusgra  48246  gpg3nbgrvtx0  48264  gpg3kgrtriexlem1  48271  logbpw2m1  48755