Theorem ltletrd 11305

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 11237	. . 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 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  lelttrdi  11307  uzwo3  12868  rpgecl  12947  fznatpl1  13506  modabs  13836  seqf1olem1  13976  expgt1  14035  leexp2a  14107  bernneq3  14166  expnbnd  14167  expmulnbnd  14170  digit1  14172  discr1  14174  hashfun  14372  seqcoll2  14400  abssubne0  15252  icodiamlt  15373  reccn2  15532  isercolllem1  15600  isumltss  15783  fprodntriv  15877  efcllem  16012  sin01bnd  16122  cos01bnd  16123  sin01gt0  16127  eirrlem  16141  rpnnen2lem11  16161  ruclem10  16176  bitsmod  16375  bitsinv1lem  16380  smuval2  16421  prmreclem5  16860  1arith  16867  2expltfac  17032  mndodconglem  19482  sylow1lem1  19539  gzrngunit  21400  nlmvscnlem1  24642  nrginvrcnlem  24647  iccpnfhmeo  24911  cnheibor  24922  evth  24926  lebnumlem1  24928  ipcnlem1  25213  lmnn  25231  ovolicc2lem2  25487  itg2monolem1  25719  itg2monolem3  25721  dvferm1lem  25956  dvcnvre  25992  dvfsumlem3  26003  dvfsumrlim  26006  plyco0  26165  aaliou2b  26317  pilem2  26430  cosq34lt1  26504  cosordlem  26507  logdivlti  26597  logdivle  26599  logcnlem3  26621  logcnlem4  26622  cxpcn3lem  26725  atanre  26863  atanlogaddlem  26891  atans2  26909  birthdaylem3  26931  cxp2lim  26955  cxploglim2  26957  jensenlem2  26966  harmonicubnd  26988  fsumharmonic  26990  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamucov  27016  ftalem2  27052  ftalem5  27055  vma1  27144  chtrpcl  27153  ppiltx  27155  fsumfldivdiaglem  27167  chtub  27191  fsumvma2  27193  chpval2  27197  chpchtsum  27198  chpub  27199  bpos1  27262  bposlem1  27263  bposlem2  27264  bposlem6  27268  gausslemma2dlem0c  27337  lgsquadlem1  27359  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chtppilim  27454  chto1ub  27455  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  rplogsumlem2  27464  dchrisumlema  27467  dchrisumlem3  27470  dchrmusumlema  27472  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0lema  27493  mulog2sumlem1  27513  chpdifbndlem1  27532  chpdifbnd  27534  pntrsumo1  27544  pntpbnd1  27565  pntpbnd2  27566  pntibndlem2  27570  pntlemb  27576  pntlemh  27578  pntlemr  27581  pntlem3  27588  pnt2  27592  ostth2lem1  27597  ostth2lem3  27614  ostth2lem4  27615  axsegconlem7  29008  axsegconlem10  29011  axlowdimlem16  29042  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  clwlkclwwlklem2a2  30080  clwwlkext2edg  30143  smatrcl  33974  1smat1  33982  lmdvg  34131  dya2icoseg  34455  eulerpartlems  34538  reprlt  34797  reprinfz1  34800  breprexplemc  34810  hgt750lemd  34826  hgt750lem  34829  hgt750leme  34836  tgoldbachgtde  34838  subfacval3  35405  knoppndvlem1  36734  knoppndvlem2  36735  knoppndvlem7  36740  knoppndvlem14  36747  knoppndvlem18  36751  poimirlem7  37878  poimirlem24  37895  poimirlem29  37900  mblfinlem2  37909  itg2addnclem  37922  itg2addnclem3  37924  ftc1anclem5  37948  ftc1anclem7  37950  ftc1anc  37952  areacirclem5  37963  lcmineqlem23  42421  3lexlogpow5ineq2  42425  3lexlogpow5ineq4  42426  3lexlogpow5ineq3  42427  aks4d1lem1  42432  dvrelog2  42434  aks4d1p1p3  42439  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  aks4d1p2  42447  aks4d1p3  42448  aks4d1p5  42450  aks4d1p6  42451  aks4d1p7d1  42452  aks4d1p7  42453  aks4d1p8d2  42455  aks4d1p8  42457  aks4d1p9  42458  posbezout  42470  hashscontpow1  42491  aks6d1c3  42493  2ap1caineq  42515  sticksstones12a  42527  sticksstones22  42538  aks6d1c7lem1  42550  aks6d1c7lem2  42551  aks6d1c7  42554  aks5lem6  42562  aks5lem8  42571  flt4lem7  43017  3cubeslem1  43041  irrapxlem4  43182  irrapxlem5  43183  pellexlem2  43187  pell14qrgapw  43233  pellqrex  43236  pellfundgt1  43240  pellfundex  43243  ltrmxnn0  43306  jm2.24nn  43316  jm2.17c  43319  jm2.24  43320  jm2.23  43353  jm3.1lem1  43374  jm3.1lem2  43375  radcnvrat  44670  dstregt0  45644  monoords  45659  uzubioo  45925  fsumnncl  45932  mullimc  45976  mullimcf  45983  sumnnodd  45990  limcleqr  46002  addlimc  46006  0ellimcdiv  46007  limclner  46009  limsupgtlem  46135  dvdivbd  46281  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnmul  46301  iblspltprt  46331  itgspltprt  46337  stoweidlem11  46369  stoweidlem24  46382  stoweidlem25  46383  stoweidlem26  46384  stoweidlem34  46392  stoweidlem36  46394  stoweidlem42  46400  stoweidlem44  46402  stoweidlem51  46409  stoweidlem59  46417  wallispi  46428  wallispi2lem1  46429  wallispi2  46431  stirlinglem11  46442  dirkertrigeqlem1  46456  dirkeritg  46460  fourierdlem10  46475  fourierdlem11  46476  fourierdlem12  46477  fourierdlem15  46480  fourierdlem19  46484  fourierdlem20  46485  fourierdlem30  46495  fourierdlem32  46497  fourierdlem40  46505  fourierdlem41  46506  fourierdlem44  46509  fourierdlem46  46510  fourierdlem47  46511  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem78  46542  fourierdlem79  46543  fourierdlem89  46553  fourierdlem92  46556  fourierdlem103  46567  fourierdlem104  46568  fouriersw  46589  etransclem4  46596  etransclem23  46615  etransclem31  46623  etransclem32  46624  etransclem35  46627  etransclem41  46633  etransclem48  46640  ioorrnopnlem  46662  sge0uzfsumgt  46802  sge0seq  46804  iundjiun  46818  carageniuncllem2  46880  hoidmvlelem3  46955  iunhoiioolem  47033  vonioolem1  47038  smfmullem1  47149  smfmullem2  47150  smfmullem3  47151  ceilhalfgt1  47689  modm2nep1  47726  modp2nep1  47727  modm1nep2  47728  modm1nem2  47729  modm1p1ne  47730  bgoldbtbndlem2  48166  gpgprismgrusgra  48418  gpg3nbgrvtx0  48436  gpg3kgrtriexlem1  48443  logbpw2m1  48927