Theorem ltletrd 11300

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 11232	. . 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 5086  ℝcr 11031   < clt 11173   ≤ cle 11174

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 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-pre-lttri 11106  ax-pre-lttrn 11107

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179

This theorem is referenced by:  lelttrdi  11302  uzwo3  12887  rpgecl  12966  fznatpl1  13526  modabs  13857  seqf1olem1  13997  expgt1  14056  leexp2a  14128  bernneq3  14187  expnbnd  14188  expmulnbnd  14191  digit1  14193  discr1  14195  hashfun  14393  seqcoll2  14421  abssubne0  15273  icodiamlt  15394  reccn2  15553  isercolllem1  15621  isumltss  15807  fprodntriv  15901  efcllem  16036  sin01bnd  16146  cos01bnd  16147  sin01gt0  16151  eirrlem  16165  rpnnen2lem11  16185  ruclem10  16200  bitsmod  16399  bitsinv1lem  16404  smuval2  16445  prmreclem5  16885  1arith  16892  2expltfac  17057  mndodconglem  19510  sylow1lem1  19567  gzrngunit  21426  nlmvscnlem1  24664  nrginvrcnlem  24669  iccpnfhmeo  24925  cnheibor  24935  evth  24939  lebnumlem1  24941  ipcnlem1  25225  lmnn  25243  ovolicc2lem2  25498  itg2monolem1  25730  itg2monolem3  25732  dvferm1lem  25964  dvcnvre  25999  dvfsumlem3  26008  dvfsumrlim  26011  plyco0  26170  aaliou2b  26321  pilem2  26433  cosq34lt1  26507  cosordlem  26510  logdivlti  26600  logdivle  26602  logcnlem3  26624  logcnlem4  26625  cxpcn3lem  26727  atanre  26865  atanlogaddlem  26893  atans2  26911  birthdaylem3  26933  cxp2lim  26957  cxploglim2  26959  jensenlem2  26968  harmonicubnd  26990  fsumharmonic  26992  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamucov  27018  ftalem2  27054  ftalem5  27057  vma1  27146  chtrpcl  27155  ppiltx  27157  fsumfldivdiaglem  27169  chtub  27192  fsumvma2  27194  chpval2  27198  chpchtsum  27199  chpub  27200  bpos1  27263  bposlem1  27264  bposlem2  27265  bposlem6  27269  gausslemma2dlem0c  27338  lgsquadlem1  27360  chebbnd1lem1  27449  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  chtppilimlem1  27453  chtppilimlem2  27454  chtppilim  27455  chto1ub  27456  chebbnd2  27457  chto1lb  27458  chpchtlim  27459  chpo1ub  27460  rplogsumlem2  27465  dchrisumlema  27468  dchrisumlem3  27471  dchrmusumlema  27473  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0lema  27494  mulog2sumlem1  27514  chpdifbndlem1  27533  chpdifbnd  27535  pntrsumo1  27545  pntpbnd1  27566  pntpbnd2  27567  pntibndlem2  27571  pntlemb  27577  pntlemh  27579  pntlemr  27582  pntlem3  27589  pnt2  27593  ostth2lem1  27598  ostth2lem3  27615  ostth2lem4  27616  axsegconlem7  29009  axsegconlem10  29012  axlowdimlem16  29043  axcontlem2  29051  axcontlem4  29053  axcontlem7  29056  clwlkclwwlklem2a2  30081  clwwlkext2edg  30144  smatrcl  33959  1smat1  33967  lmdvg  34116  dya2icoseg  34440  eulerpartlems  34523  reprlt  34782  reprinfz1  34785  breprexplemc  34795  hgt750lemd  34811  hgt750lem  34814  hgt750leme  34821  tgoldbachgtde  34823  subfacval3  35390  knoppndvlem1  36791  knoppndvlem2  36792  knoppndvlem7  36797  knoppndvlem14  36804  knoppndvlem18  36808  poimirlem7  37965  poimirlem24  37982  poimirlem29  37987  mblfinlem2  37996  itg2addnclem  38009  itg2addnclem3  38011  ftc1anclem5  38035  ftc1anclem7  38037  ftc1anc  38039  areacirclem5  38050  lcmineqlem23  42507  3lexlogpow5ineq2  42511  3lexlogpow5ineq4  42512  3lexlogpow5ineq3  42513  aks4d1lem1  42518  dvrelog2  42520  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  aks4d1p2  42533  aks4d1p3  42534  aks4d1p5  42536  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8d2  42541  aks4d1p8  42543  aks4d1p9  42544  posbezout  42556  hashscontpow1  42577  aks6d1c3  42579  2ap1caineq  42601  sticksstones12a  42613  sticksstones22  42624  aks6d1c7lem1  42636  aks6d1c7lem2  42637  aks6d1c7  42640  aks5lem6  42648  aks5lem8  42657  flt4lem7  43109  3cubeslem1  43133  irrapxlem4  43274  irrapxlem5  43275  pellexlem2  43279  pell14qrgapw  43325  pellqrex  43328  pellfundgt1  43332  pellfundex  43335  ltrmxnn0  43398  jm2.24nn  43408  jm2.17c  43411  jm2.24  43412  jm2.23  43445  jm3.1lem1  43466  jm3.1lem2  43467  radcnvrat  44762  dstregt0  45736  monoords  45751  uzubioo  46016  fsumnncl  46023  mullimc  46067  mullimcf  46074  sumnnodd  46081  limcleqr  46093  addlimc  46097  0ellimcdiv  46098  limclner  46100  limsupgtlem  46226  dvdivbd  46372  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  iblspltprt  46422  itgspltprt  46428  stoweidlem11  46460  stoweidlem24  46473  stoweidlem25  46474  stoweidlem26  46475  stoweidlem34  46483  stoweidlem36  46485  stoweidlem42  46491  stoweidlem44  46493  stoweidlem51  46500  stoweidlem59  46508  wallispi  46519  wallispi2lem1  46520  wallispi2  46522  stirlinglem11  46533  dirkertrigeqlem1  46547  dirkeritg  46551  fourierdlem10  46566  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem19  46575  fourierdlem20  46576  fourierdlem30  46586  fourierdlem32  46588  fourierdlem40  46596  fourierdlem41  46597  fourierdlem44  46600  fourierdlem46  46601  fourierdlem47  46602  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem78  46633  fourierdlem79  46634  fourierdlem89  46644  fourierdlem92  46647  fourierdlem103  46658  fourierdlem104  46659  fouriersw  46680  etransclem4  46687  etransclem23  46706  etransclem31  46714  etransclem32  46715  etransclem35  46718  etransclem41  46724  etransclem48  46731  ioorrnopnlem  46753  sge0uzfsumgt  46893  sge0seq  46895  iundjiun  46909  carageniuncllem2  46971  hoidmvlelem3  47046  iunhoiioolem  47124  vonioolem1  47129  smfmullem1  47240  smfmullem2  47241  smfmullem3  47242  ceilhalfgt1  47796  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  bgoldbtbndlem2  48297  gpgprismgrusgra  48549  gpg3nbgrvtx0  48567  gpg3kgrtriexlem1  48574  logbpw2m1  49058