Theorem lelttrd 11395

Description: Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
lelttrd.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)
lelttrd.5	⊢ (𝜑 → 𝐵 < 𝐶)

Assertion

Ref	Expression
lelttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem lelttrd

Step	Hyp	Ref	Expression
1		lelttrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		lelttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		lelttr 11327	. . 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 2145   class class class wbr 5103  ℝcr 11126   < clt 11270   ≤ cle 11271

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276

This theorem is used by:  lt2msq1  12126  suprzcl  12704  ge0p1rp  13078  elfzolt3  13728  flflp1  13871  ltdifltdiv  13898  modsubdir  14007  seqf1olem1  14108  seqf1olem2  14109  expmulnbnd  14302  discr1  14306  faclbnd5  14365  bcp1nk  14384  hashfun  14505  swrds2  15014  abslt  15405  abs3lem  15429  fzomaxdiflem  15433  icodiamlt  15528  reccn2  15687  o1rlimmul  15709  caucvgrlem  15763  geomulcvg  15968  mertenslem1  15976  bpoly4  16148  ef01bndlem  16275  sin01bnd  16276  cos01bnd  16277  sinltx  16280  eirrlem  16295  rpnnen2lem11  16315  ruclem10  16330  bitsfzolem  16527  bitsfzo  16528  bitsinv1lem  16534  smueqlem  16583  pcfaclem  16993  pockthg  17001  prmreclem5  17015  1arith  17022  4sqlem11  17050  4sqlem12  17051  4sqlem13  17052  coe1tmmul2  22505  ssblex  24657  nlmvscnlem2  24914  nlmvscnlem1  24915  nrginvrcnlem  24920  blcvx  25027  icccmplem2  25053  reconnlem2  25057  metdcnlem  25066  icopnfcnv  25173  nmoleub2lem3  25346  ipcnlem2  25475  ipcnlem1  25476  minveclem3b  25659  minveclem3  25660  pjthlem1  25668  pmltpclem2  25680  ivthlem2  25683  ovollb2lem  25719  iundisj  25779  uniioombllem3  25816  opnmbllem  25832  itg2monolem3  25983  itg2cnlem2  25993  dveflem  26209  dvferm2lem  26216  lhop1lem  26243  dvcnvre  26249  ftc1a  26267  ftc1lem4  26269  coeeulem  26453  dgradd2  26497  aaliou2b  26580  ulmdvlem1  26639  itgulm  26647  radcnvlem1  26652  radcnvlt1  26657  radcnvle  26659  psercnlem1  26664  pserdvlem1  26666  pserdv  26668  abelthlem2  26671  abelthlem7  26677  cosordlem  26770  tanord1  26777  efif1olem1  26782  logcnlem3  26884  logcnlem4  26885  efopnlem1  26896  logtayl  26900  cxpcn3lem  26987  birthdaylem3  27193  efrlim  27209  lgamgulmlem2  27269  lgamucov  27277  ftalem1  27312  ftalem2  27313  ftalem5  27316  basellem1  27320  basellem3  27322  perfectlem2  27469  bposlem1  27523  bposlem3  27525  bposlem6  27528  lgsdirprm  27570  lgsqrlem2  27586  lgseisen  27618  lgsquadlem1  27619  lgsquadlem2  27620  2sqlem8  27665  2sqblem  27670  dchrvmasumiflem1  27740  pntrmax  27803  pntlemc  27834  pntlemg  27837  pntlemr  27841  axpaschlem  29400  axlowdimlem16  29417  clwwisshclwwslem  30487  smcnlem  31181  minvecolem3  31360  pjhthlem1  31875  nmcexi  32510  iundisjf  33065  iundisjfi  33270  psgnfzto1stlem  33543  esplyfval2  34078  esplyfval3  34085  cos9thpiminplylem1  34295  dya2icoseg  34791  reprgt  35132  hgt750lem  35162  tgoldbachgtde  35171  subfaclim  35770  bcprod  36320  dnicn  37192  unbdqndv2lem1  37209  unbdqndv2lem2  37210  knoppndvlem18  37229  poimirlem6  38378  poimirlem7  38379  poimirlem12  38384  poimirlem15  38387  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem23  38395  poimirlem24  38396  opnmbllem0  38408  mblfinlem3  38411  mblfinlem4  38412  ftc1cnnclem  38443  ftc1anclem7  38451  isbnd3  38537  cntotbnd  38549  rrnequiv  38588  aks4d1p1p3  42938  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p5  42949  posbezout  42969  primrootlekpowne0  42974  aks6d1c5lem1  43005  2np3bcnp1  43013  sticksstones10  43024  sticksstones12a  43026  sticksstones22  43037  aks6d1c7lem1  43049  unitscyglem2  43065  flt4lem7  43508  fltnltalem  43511  fltnlta  43512  irrapxlem1  43666  pell14qrgapw  43720  monotoddzzfi  43786  ltrmynn0  43792  jm2.24nn  43803  acongeq  43827  jm2.26lem3  43845  jm3.1lem2  43862  binomcxplemnotnn0  45183  isosctrlem1ALT  45759  rfcnnnub  45873  zltlesub  46121  monoords  46133  supxrge  46171  infleinflem2  46203  uzubioo  46398  fmul01lt1lem1  46417  fmul01lt1lem2  46418  lptre2pt  46471  addlimc  46479  0ellimcdiv  46480  limclner  46482  climleltrp  46507  limsupubuzlem  46543  limsup10exlem  46603  icccncfext  46718  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnmul  46774  iblspltprt  46804  itgspltprt  46810  stoweidlem5  46836  stoweidlem11  46842  stoweidlem13  46844  stoweidlem14  46845  stoweidlem25  46856  stoweidlem26  46857  stoweidlem42  46873  stoweidlem59  46890  stoweid  46894  wallispilem3  46898  wallispilem4  46899  wallispilem5  46900  fourierdlem10  46948  fourierdlem11  46949  fourierdlem12  46950  fourierdlem15  46953  fourierdlem20  46958  fourierdlem24  46962  fourierdlem30  46968  fourierdlem31  46969  fourierdlem33  46971  fourierdlem40  46978  fourierdlem41  46979  fourierdlem42  46980  fourierdlem43  46981  fourierdlem44  46982  fourierdlem46  46983  fourierdlem47  46984  fourierdlem48  46985  fourierdlem50  46987  fourierdlem63  47000  fourierdlem64  47001  fourierdlem65  47002  fourierdlem73  47010  fourierdlem74  47011  fourierdlem75  47012  fourierdlem76  47013  fourierdlem77  47014  fourierdlem78  47015  fourierdlem79  47016  fourierdlem87  47024  fourierdlem91  47028  fourierdlem92  47029  fourierdlem103  47040  fourierdlem104  47041  fouriersw  47062  etransclem19  47084  etransclem23  47088  etransclem48  47113  ioorrnopnlem  47135  iundjiun  47291  omeiunltfirp  47350  caratheodorylem1  47357  hoicvr  47379  hoidmv1lelem2  47423  hoidmvlelem2  47427  hoiqssbllem2  47454  vonioolem1  47511  vonicclem1  47514  smflimlem4  47605  smfmullem1  47622  2tceilhalfelfzo1  48227  addmodne  48241  2timesltsqm1  48270  iccpartgt  48330  perfectALTVlem2  48641  bgoldbtbndlem2  48725  pgrple2abl  49298  logbpw2m1  49500  dignn0ldlem  49535  2itscp  49714