Theorem ltletrd 11297

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5099  ℝcr 11029   < clt 11170   ≤ cle 11171

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-pre-lttri 11104  ax-pre-lttrn 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  lelttrdi  11299  uzwo3  12860  rpgecl  12939  fznatpl1  13498  modabs  13828  seqf1olem1  13968  expgt1  14027  leexp2a  14099  bernneq3  14158  expnbnd  14159  expmulnbnd  14162  digit1  14164  discr1  14166  hashfun  14364  seqcoll2  14392  abssubne0  15244  icodiamlt  15365  reccn2  15524  isercolllem1  15592  isumltss  15775  fprodntriv  15869  efcllem  16004  sin01bnd  16114  cos01bnd  16115  sin01gt0  16119  eirrlem  16133  rpnnen2lem11  16153  ruclem10  16168  bitsmod  16367  bitsinv1lem  16372  smuval2  16413  prmreclem5  16852  1arith  16859  2expltfac  17024  mndodconglem  19474  sylow1lem1  19531  gzrngunit  21392  nlmvscnlem1  24634  nrginvrcnlem  24639  iccpnfhmeo  24903  cnheibor  24914  evth  24918  lebnumlem1  24920  ipcnlem1  25205  lmnn  25223  ovolicc2lem2  25479  itg2monolem1  25711  itg2monolem3  25713  dvferm1lem  25948  dvcnvre  25984  dvfsumlem3  25995  dvfsumrlim  25998  plyco0  26157  aaliou2b  26309  pilem2  26422  cosq34lt1  26496  cosordlem  26499  logdivlti  26589  logdivle  26591  logcnlem3  26613  logcnlem4  26614  cxpcn3lem  26717  atanre  26855  atanlogaddlem  26883  atans2  26901  birthdaylem3  26923  cxp2lim  26947  cxploglim2  26949  jensenlem2  26958  harmonicubnd  26980  fsumharmonic  26982  lgamgulmlem2  27000  lgamgulmlem3  27001  lgamucov  27008  ftalem2  27044  ftalem5  27047  vma1  27136  chtrpcl  27145  ppiltx  27147  fsumfldivdiaglem  27159  chtub  27183  fsumvma2  27185  chpval2  27189  chpchtsum  27190  chpub  27191  bpos1  27254  bposlem1  27255  bposlem2  27256  bposlem6  27260  gausslemma2dlem0c  27329  lgsquadlem1  27351  chebbnd1lem1  27440  chebbnd1lem2  27441  chebbnd1lem3  27442  chebbnd1  27443  chtppilimlem1  27444  chtppilimlem2  27445  chtppilim  27446  chto1ub  27447  chebbnd2  27448  chto1lb  27449  chpchtlim  27450  chpo1ub  27451  rplogsumlem2  27456  dchrisumlema  27459  dchrisumlem3  27462  dchrmusumlema  27464  dchrvmasumlem2  27469  dchrvmasumiflem1  27472  dchrisum0lema  27485  mulog2sumlem1  27505  chpdifbndlem1  27524  chpdifbnd  27526  pntrsumo1  27536  pntpbnd1  27557  pntpbnd2  27558  pntibndlem2  27562  pntlemb  27568  pntlemh  27570  pntlemr  27573  pntlem3  27580  pnt2  27584  ostth2lem1  27589  ostth2lem3  27606  ostth2lem4  27607  axsegconlem7  28979  axsegconlem10  28982  axlowdimlem16  29013  axcontlem2  29021  axcontlem4  29023  axcontlem7  29026  clwlkclwwlklem2a2  30051  clwwlkext2edg  30114  smatrcl  33934  1smat1  33942  lmdvg  34091  dya2icoseg  34415  eulerpartlems  34498  reprlt  34757  reprinfz1  34760  breprexplemc  34770  hgt750lemd  34786  hgt750lem  34789  hgt750leme  34796  tgoldbachgtde  34798  subfacval3  35364  knoppndvlem1  36687  knoppndvlem2  36688  knoppndvlem7  36693  knoppndvlem14  36700  knoppndvlem18  36704  poimirlem7  37799  poimirlem24  37816  poimirlem29  37821  mblfinlem2  37830  itg2addnclem  37843  itg2addnclem3  37845  ftc1anclem5  37869  ftc1anclem7  37871  ftc1anc  37873  areacirclem5  37884  lcmineqlem23  42342  3lexlogpow5ineq2  42346  3lexlogpow5ineq4  42347  3lexlogpow5ineq3  42348  aks4d1lem1  42353  dvrelog2  42355  aks4d1p1p3  42360  aks4d1p1p2  42361  aks4d1p1p4  42362  aks4d1p1p6  42364  aks4d1p1p7  42365  aks4d1p1p5  42366  aks4d1p1  42367  aks4d1p2  42368  aks4d1p3  42369  aks4d1p5  42371  aks4d1p6  42372  aks4d1p7d1  42373  aks4d1p7  42374  aks4d1p8d2  42376  aks4d1p8  42378  aks4d1p9  42379  posbezout  42391  hashscontpow1  42412  aks6d1c3  42414  2ap1caineq  42436  sticksstones12a  42448  sticksstones22  42459  aks6d1c7lem1  42471  aks6d1c7lem2  42472  aks6d1c7  42475  aks5lem6  42483  aks5lem8  42492  flt4lem7  42938  3cubeslem1  42962  irrapxlem4  43103  irrapxlem5  43104  pellexlem2  43108  pell14qrgapw  43154  pellqrex  43157  pellfundgt1  43161  pellfundex  43164  ltrmxnn0  43227  jm2.24nn  43237  jm2.17c  43240  jm2.24  43241  jm2.23  43274  jm3.1lem1  43295  jm3.1lem2  43296  radcnvrat  44591  dstregt0  45566  monoords  45581  uzubioo  45847  fsumnncl  45854  mullimc  45898  mullimcf  45905  sumnnodd  45912  limcleqr  45924  addlimc  45928  0ellimcdiv  45929  limclner  45931  limsupgtlem  46057  dvdivbd  46203  ioodvbdlimc1lem1  46211  ioodvbdlimc1lem2  46212  ioodvbdlimc2lem  46214  dvnmul  46223  iblspltprt  46253  itgspltprt  46259  stoweidlem11  46291  stoweidlem24  46304  stoweidlem25  46305  stoweidlem26  46306  stoweidlem34  46314  stoweidlem36  46316  stoweidlem42  46322  stoweidlem44  46324  stoweidlem51  46331  stoweidlem59  46339  wallispi  46350  wallispi2lem1  46351  wallispi2  46353  stirlinglem11  46364  dirkertrigeqlem1  46378  dirkeritg  46382  fourierdlem10  46397  fourierdlem11  46398  fourierdlem12  46399  fourierdlem15  46402  fourierdlem19  46406  fourierdlem20  46407  fourierdlem30  46417  fourierdlem32  46419  fourierdlem40  46427  fourierdlem41  46428  fourierdlem44  46431  fourierdlem46  46432  fourierdlem47  46433  fourierdlem48  46434  fourierdlem49  46435  fourierdlem50  46436  fourierdlem63  46449  fourierdlem64  46450  fourierdlem65  46451  fourierdlem74  46460  fourierdlem75  46461  fourierdlem76  46462  fourierdlem78  46464  fourierdlem79  46465  fourierdlem89  46475  fourierdlem92  46478  fourierdlem103  46489  fourierdlem104  46490  fouriersw  46511  etransclem4  46518  etransclem23  46537  etransclem31  46545  etransclem32  46546  etransclem35  46549  etransclem41  46555  etransclem48  46562  ioorrnopnlem  46584  sge0uzfsumgt  46724  sge0seq  46726  iundjiun  46740  carageniuncllem2  46802  hoidmvlelem3  46877  iunhoiioolem  46955  vonioolem1  46960  smfmullem1  47071  smfmullem2  47072  smfmullem3  47073  ceilhalfgt1  47611  modm2nep1  47648  modp2nep1  47649  modm1nep2  47650  modm1nem2  47651  modm1p1ne  47652  bgoldbtbndlem2  48088  gpgprismgrusgra  48340  gpg3nbgrvtx0  48358  gpg3kgrtriexlem1  48365  logbpw2m1  48849