Theorem ltletrd 11421

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301

This theorem is referenced by:  lelttrdi  11423  uzwo3  12985  rpgecl  13063  fznatpl1  13618  modabs  13944  seqf1olem1  14082  expgt1  14141  leexp2a  14212  bernneq3  14270  expnbnd  14271  expmulnbnd  14274  digit1  14276  discr1  14278  hashfun  14476  seqcoll2  14504  abssubne0  15355  icodiamlt  15474  reccn2  15633  isercolllem1  15701  isumltss  15884  fprodntriv  15978  efcllem  16113  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  eirrlem  16240  rpnnen2lem11  16260  ruclem10  16275  bitsmod  16473  bitsinv1lem  16478  smuval2  16519  prmreclem5  16958  1arith  16965  2expltfac  17130  mndodconglem  19559  sylow1lem1  19616  gzrngunit  21451  nlmvscnlem1  24707  nrginvrcnlem  24712  iccpnfhmeo  24976  cnheibor  24987  evth  24991  lebnumlem1  24993  ipcnlem1  25279  lmnn  25297  ovolicc2lem2  25553  itg2monolem1  25785  itg2monolem3  25787  dvferm1lem  26022  dvcnvre  26058  dvfsumlem3  26069  dvfsumrlim  26072  plyco0  26231  aaliou2b  26383  pilem2  26496  cosq34lt1  26569  cosordlem  26572  logdivlti  26662  logdivle  26664  logcnlem3  26686  logcnlem4  26687  cxpcn3lem  26790  atanre  26928  atanlogaddlem  26956  atans2  26974  birthdaylem3  26996  cxp2lim  27020  cxploglim2  27022  jensenlem2  27031  harmonicubnd  27053  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamucov  27081  ftalem2  27117  ftalem5  27120  vma1  27209  chtrpcl  27218  ppiltx  27220  fsumfldivdiaglem  27232  chtub  27256  fsumvma2  27258  chpval2  27262  chpchtsum  27263  chpub  27264  bpos1  27327  bposlem1  27328  bposlem2  27329  bposlem6  27333  gausslemma2dlem0c  27402  lgsquadlem1  27424  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chtppilimlem2  27518  chtppilim  27519  chto1ub  27520  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ub  27524  rplogsumlem2  27529  dchrisumlema  27532  dchrisumlem3  27535  dchrmusumlema  27537  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0lema  27558  mulog2sumlem1  27578  chpdifbndlem1  27597  chpdifbnd  27599  pntrsumo1  27609  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntlemb  27641  pntlemh  27643  pntlemr  27646  pntlem3  27653  pnt2  27657  ostth2lem1  27662  ostth2lem3  27679  ostth2lem4  27680  axsegconlem7  28938  axsegconlem10  28941  axlowdimlem16  28972  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  clwlkclwwlklem2a2  30012  clwwlkext2edg  30075  smatrcl  33795  1smat1  33803  lmdvg  33952  dya2icoseg  34279  eulerpartlems  34362  reprlt  34634  reprinfz1  34637  breprexplemc  34647  hgt750lemd  34663  hgt750lem  34666  hgt750leme  34673  tgoldbachgtde  34675  subfacval3  35194  knoppndvlem1  36513  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem14  36526  knoppndvlem18  36530  poimirlem7  37634  poimirlem24  37651  poimirlem29  37656  mblfinlem2  37665  itg2addnclem  37678  itg2addnclem3  37680  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anc  37708  areacirclem5  37719  lcmineqlem23  42052  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow5ineq3  42058  aks4d1lem1  42063  dvrelog2  42065  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  hashscontpow1  42122  aks6d1c3  42124  2ap1caineq  42146  sticksstones12a  42158  sticksstones22  42169  aks6d1c7lem1  42181  aks6d1c7lem2  42182  aks6d1c7  42185  aks5lem6  42193  aks5lem8  42202  metakunt6  42211  metakunt11  42216  metakunt27  42232  metakunt28  42233  flt4lem7  42669  3cubeslem1  42695  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pell14qrgapw  42887  pellqrex  42890  pellfundgt1  42894  pellfundex  42897  ltrmxnn0  42961  jm2.24nn  42971  jm2.17c  42974  jm2.24  42975  jm2.23  43008  jm3.1lem1  43029  jm3.1lem2  43030  radcnvrat  44333  dstregt0  45293  monoords  45309  uzubioo  45580  fsumnncl  45587  mullimc  45631  mullimcf  45638  sumnnodd  45645  limcleqr  45659  addlimc  45663  0ellimcdiv  45664  limclner  45666  limsupgtlem  45792  dvdivbd  45938  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  iblspltprt  45988  itgspltprt  45994  stoweidlem11  46026  stoweidlem24  46039  stoweidlem25  46040  stoweidlem26  46041  stoweidlem34  46049  stoweidlem36  46051  stoweidlem42  46057  stoweidlem44  46059  stoweidlem51  46066  stoweidlem59  46074  wallispi  46085  wallispi2lem1  46086  wallispi2  46088  stirlinglem11  46099  dirkertrigeqlem1  46113  dirkeritg  46117  fourierdlem10  46132  fourierdlem11  46133  fourierdlem12  46134  fourierdlem15  46137  fourierdlem19  46141  fourierdlem20  46142  fourierdlem30  46152  fourierdlem32  46154  fourierdlem40  46162  fourierdlem41  46163  fourierdlem44  46166  fourierdlem46  46167  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem89  46210  fourierdlem92  46213  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  etransclem4  46253  etransclem23  46272  etransclem31  46280  etransclem32  46281  etransclem35  46284  etransclem41  46290  etransclem48  46297  ioorrnopnlem  46319  sge0uzfsumgt  46459  sge0seq  46461  iundjiun  46475  carageniuncllem2  46537  hoidmvlelem3  46612  iunhoiioolem  46690  vonioolem1  46695  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  bgoldbtbndlem2  47793  gpg3nbgrvtx0  48032  gpg3kgrtriexlem1  48039  logbpw2m1  48488