Theorem ltletrd 11477

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ℝcr 11206   < clt 11350   ≤ cle 11351

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-pre-lttri 11281  ax-pre-lttrn 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8725  df-en 8982  df-dom 8983  df-sdom 8984  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356

This theorem is used by:  lelttrdi  11479  uzwo3  13077  rpgecl  13157  fznatpl1  13719  modabs  14051  seqf1olem1  14191  expgt1  14250  leexp2a  14322  bernneq3  14382  expnbnd  14383  expmulnbnd  14386  digit1  14388  discr1  14390  hashfun  14589  seqcoll2  14617  abssubne0  15493  icodiamlt  15614  reccn2  15773  isercolllem1  15841  isumltss  16026  fprodntriv  16118  efcllem  16252  sin01bnd  16362  cos01bnd  16363  sin01gt0  16367  eirrlem  16381  rpnnen2lem11  16401  ruclem10  16416  bitsmod  16615  bitsinv1lem  16620  smuval2  16661  prmreclem5  17107  1arith  17114  2expltfac  17279  mndodconglem  19764  sylow1lem1  19821  gzrngunit  21748  nlmvscnlem1  25014  nrginvrcnlem  25019  iccpnfhmeo  25275  cnheibor  25285  evth  25289  lebnumlem1  25291  ipcnlem1  25575  lmnn  25593  ovolicc2lem2  25848  itg2monolem1  26080  itg2monolem3  26082  dvferm1lem  26313  dvcnvre  26348  dvfsumlem3  26357  dvfsumrlim  26360  plyco0  26519  aaliou2b  26677  pilem2  26788  cosq34lt1  26864  cosordlem  26867  logdivlti  26957  logdivle  26959  logcnlem3  26981  logcnlem4  26982  cxpcn3lem  27084  atanre  27222  atanlogaddlem  27250  atans2  27268  birthdaylem3  27290  cxp2lim  27313  cxploglim2  27315  jensenlem2  27324  harmonicubnd  27346  fsumharmonic  27348  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamucov  27374  ftalem2  27410  ftalem5  27413  vma1  27502  chtrpcl  27511  ppiltx  27513  fsumfldivdiaglem  27525  chtub  27548  fsumvma2  27550  chpval2  27554  chpchtsum  27555  chpub  27556  bpos1  27619  bposlem1  27620  bposlem2  27621  bposlem6  27625  gausslemma2dlem0c  27694  lgsquadlem1  27716  chebbnd1lem1  27805  chebbnd1lem2  27806  chebbnd1lem3  27807  chebbnd1  27808  chtppilimlem1  27809  chtppilimlem2  27810  chtppilim  27811  chto1ub  27812  chebbnd2  27813  chto1lb  27814  chpchtlim  27815  chpo1ub  27816  rplogsumlem2  27821  dchrisumlema  27824  dchrisumlem3  27827  dchrmusumlema  27829  dchrvmasumlem2  27834  dchrvmasumiflem1  27837  dchrisum0lema  27850  mulog2sumlem1  27870  chpdifbndlem1  27889  chpdifbnd  27891  pntrsumo1  27901  pntpbnd1  27922  pntpbnd2  27923  pntibndlem2  27927  pntlemb  27933  pntlemh  27935  pntlemr  27938  pntlem3  27945  pnt2  27949  ostth2lem1  27954  ostth2lem3  27971  ostth2lem4  27972  axsegconlem7  29510  axsegconlem10  29513  axlowdimlem16  29544  axcontlem2  29552  axcontlem4  29554  axcontlem7  29557  clwlkclwwlklem2a2  30593  clwwlkext2edg  30656  smatrcl  34478  1smat1  34486  lmdvg  34635  dya2icoseg  34959  eulerpartlems  35042  reprlt  35298  reprinfz1  35301  breprexplemc  35311  hgt750lemd  35327  hgt750lem  35330  hgt750leme  35337  tgoldbachgtde  35339  subfacval3  36072  knoppndvlem1  37502  knoppndvlem2  37503  knoppndvlem7  37508  knoppndvlem14  37515  knoppndvlem18  37519  poimirlem7  38682  poimirlem24  38699  poimirlem29  38704  mblfinlem2  38713  itg2addnclem  38726  itg2addnclem3  38728  ftc1anclem5  38752  ftc1anclem7  38754  ftc1anc  38756  areacirclem5  38767  lcmineqlem23  43238  3lexlogpow5ineq2  43242  3lexlogpow5ineq4  43243  3lexlogpow5ineq3  43244  aks4d1lem1  43249  dvrelog2  43251  aks4d1p1p3  43256  aks4d1p1p2  43257  aks4d1p1p4  43258  aks4d1p1p6  43260  aks4d1p1p7  43261  aks4d1p1p5  43262  aks4d1p1  43263  aks4d1p2  43264  aks4d1p3  43265  aks4d1p5  43267  aks4d1p6  43268  aks4d1p7d1  43269  aks4d1p7  43270  aks4d1p8d2  43272  aks4d1p8  43274  aks4d1p9  43275  posbezout  43287  hashscontpow1  43308  aks6d1c3  43310  2ap1caineq  43332  sticksstones12a  43344  sticksstones22  43355  aks6d1c7lem1  43367  aks6d1c7lem2  43368  aks6d1c7  43371  aks5lem6  43379  aks5lem8  43388  3cubeslem1  43831  irrapxlem4  43969  irrapxlem5  43970  pellexlem2  43974  pell14qrgapw  44020  pellqrex  44023  pellfundgt1  44027  pellfundex  44030  ltrmxnn0  44093  jm2.24nn  44103  jm2.17c  44106  jm2.24  44107  jm2.23  44140  jm3.1lem1  44161  jm3.1lem2  44162  radcnvrat  45435  dstregt0  46434  monoords  46449  uzubioo  46713  fsumnncl  46720  mullimc  46764  mullimcf  46771  sumnnodd  46778  limcleqr  46790  addlimc  46794  0ellimcdiv  46795  limclner  46797  limsupgtlem  46923  dvdivbd  47069  ioodvbdlimc1lem1  47077  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  dvnmul  47089  iblspltprt  47119  itgspltprt  47125  stoweidlem11  47157  stoweidlem24  47170  stoweidlem25  47171  stoweidlem26  47172  stoweidlem34  47180  stoweidlem36  47182  stoweidlem42  47188  stoweidlem44  47190  stoweidlem51  47197  stoweidlem59  47205  wallispi  47216  wallispi2lem1  47217  wallispi2  47219  stirlinglem11  47230  dirkertrigeqlem1  47244  dirkeritg  47248  fourierdlem10  47263  fourierdlem11  47264  fourierdlem12  47265  fourierdlem15  47268  fourierdlem19  47272  fourierdlem20  47273  fourierdlem30  47283  fourierdlem32  47285  fourierdlem40  47293  fourierdlem41  47294  fourierdlem44  47297  fourierdlem46  47298  fourierdlem47  47299  fourierdlem48  47300  fourierdlem49  47301  fourierdlem50  47302  fourierdlem63  47315  fourierdlem64  47316  fourierdlem65  47317  fourierdlem74  47326  fourierdlem75  47327  fourierdlem76  47328  fourierdlem78  47330  fourierdlem79  47331  fourierdlem89  47341  fourierdlem92  47344  fourierdlem103  47355  fourierdlem104  47356  fouriersw  47377  etransclem4  47384  etransclem23  47403  etransclem31  47411  etransclem32  47412  etransclem35  47415  etransclem41  47421  etransclem48  47428  ioorrnopnlem  47450  sge0uzfsumgt  47590  sge0seq  47592  iundjiun  47606  carageniuncllem2  47668  hoidmvlelem3  47743  iunhoiioolem  47821  vonioolem1  47826  smfmullem1  47937  smfmullem2  47938  smfmullem3  47939  ceilhalfgt1  48539  modm2nep1  48578  modp2nep1  48579  modm1nep2  48580  modm1nem2  48581  modm1p1ne  48582  bgoldbtbndlem2  49040  gpgprismgrusgra  49292  gpg3nbgrvtx0  49310  gpg3kgrtriexlem1  49317  logbpw2m1  49815