Theorem lelttrd 10787

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525   < clt 10664   ≤ cle 10665

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670

This theorem is referenced by:  lt2msq1  11513  suprzcl  12050  ge0p1rp  12408  elfzolt3  13043  flflp1  13172  ltdifltdiv  13199  modsubdir  13303  seqf1olem1  13405  seqf1olem2  13406  expmulnbnd  13592  discr1  13596  faclbnd5  13654  bcp1nk  13673  hashfun  13794  swrds2  14293  abslt  14666  abs3lem  14690  fzomaxdiflem  14694  icodiamlt  14787  reccn2  14945  o1rlimmul  14967  caucvgrlem  15021  geomulcvg  15224  mertenslem1  15232  bpoly4  15405  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  sinltx  15534  eirrlem  15549  rpnnen2lem11  15569  ruclem10  15584  bitsfzolem  15773  bitsfzo  15774  bitsinv1lem  15780  smueqlem  15829  pcfaclem  16224  pockthg  16232  prmreclem5  16246  1arith  16253  4sqlem11  16281  4sqlem12  16282  4sqlem13  16283  coe1tmmul2  20905  ssblex  23035  nlmvscnlem2  23291  nlmvscnlem1  23292  nrginvrcnlem  23297  blcvx  23403  icccmplem2  23428  reconnlem2  23432  metdcnlem  23441  icopnfcnv  23547  nmoleub2lem3  23720  ipcnlem2  23848  ipcnlem1  23849  minveclem3b  24032  minveclem3  24033  pjthlem1  24041  pmltpclem2  24053  ivthlem2  24056  ovollb2lem  24092  iundisj  24152  uniioombllem3  24189  opnmbllem  24205  itg2monolem3  24356  itg2cnlem2  24366  dveflem  24582  dvferm2lem  24589  lhop1lem  24616  dvcnvre  24622  ftc1a  24640  ftc1lem4  24642  coeeulem  24821  dgradd2  24865  aaliou2b  24937  ulmdvlem1  24995  itgulm  25003  radcnvlem1  25008  radcnvlt1  25013  radcnvle  25015  psercnlem1  25020  pserdvlem1  25022  pserdv  25024  abelthlem2  25027  abelthlem7  25033  cosordlem  25122  tanord1  25129  efif1olem1  25134  logcnlem3  25235  logcnlem4  25236  efopnlem1  25247  logtayl  25251  cxpcn3lem  25336  birthdaylem3  25539  efrlim  25555  lgamgulmlem2  25615  lgamucov  25623  ftalem1  25658  ftalem2  25659  ftalem5  25662  basellem1  25666  basellem3  25668  perfectlem2  25814  bposlem1  25868  bposlem3  25870  bposlem6  25873  lgsdirprm  25915  lgsqrlem2  25931  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  2sqlem8  26010  2sqblem  26015  dchrvmasumiflem1  26085  pntrmax  26148  pntlemc  26179  pntlemg  26182  pntlemr  26186  axpaschlem  26734  axlowdimlem16  26751  clwwisshclwwslem  27799  smcnlem  28480  minvecolem3  28659  pjhthlem1  29174  nmcexi  29809  iundisjf  30352  iundisjfi  30545  psgnfzto1stlem  30792  dya2icoseg  31645  reprgt  32002  hgt750lem  32032  tgoldbachgtde  32041  subfaclim  32548  bcprod  33083  dnicn  33944  unbdqndv2lem1  33961  unbdqndv2lem2  33962  knoppndvlem18  33981  poimirlem6  35063  poimirlem7  35064  poimirlem12  35069  poimirlem15  35072  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  poimirlem24  35081  opnmbllem0  35093  mblfinlem3  35096  mblfinlem4  35097  ftc1cnnclem  35128  ftc1anclem7  35136  isbnd3  35222  cntotbnd  35234  rrnequiv  35273  2np3bcnp1  39348  metakunt1  39350  metakunt12  39361  metakunt28  39377  metakunt30  39379  fltnltalem  39618  fltnlta  39619  irrapxlem1  39763  pell14qrgapw  39817  monotoddzzfi  39883  ltrmynn0  39889  jm2.24nn  39900  acongeq  39924  jm2.26lem3  39942  jm3.1lem2  39959  binomcxplemnotnn0  41060  isosctrlem1ALT  41640  rfcnnnub  41665  zltlesub  41916  monoords  41929  supxrge  41970  infleinflem2  42003  uzubioo  42204  fmul01lt1lem1  42226  fmul01lt1lem2  42227  lptre2pt  42282  addlimc  42290  0ellimcdiv  42291  limclner  42293  climleltrp  42318  limsupubuzlem  42354  limsup10exlem  42414  icccncfext  42529  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnmul  42585  iblspltprt  42615  itgspltprt  42621  stoweidlem5  42647  stoweidlem11  42653  stoweidlem13  42655  stoweidlem14  42656  stoweidlem25  42667  stoweidlem26  42668  stoweidlem42  42684  stoweidlem59  42701  stoweid  42705  wallispilem3  42709  wallispilem4  42710  wallispilem5  42711  fourierdlem10  42759  fourierdlem11  42760  fourierdlem12  42761  fourierdlem15  42764  fourierdlem20  42769  fourierdlem24  42773  fourierdlem30  42779  fourierdlem31  42780  fourierdlem33  42782  fourierdlem40  42789  fourierdlem41  42790  fourierdlem42  42791  fourierdlem43  42792  fourierdlem44  42793  fourierdlem46  42794  fourierdlem47  42795  fourierdlem48  42796  fourierdlem50  42798  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem77  42825  fourierdlem78  42826  fourierdlem79  42827  fourierdlem87  42835  fourierdlem91  42839  fourierdlem92  42840  fourierdlem103  42851  fourierdlem104  42852  fouriersw  42873  etransclem19  42895  etransclem23  42899  etransclem48  42924  ioorrnopnlem  42946  iundjiun  43099  omeiunltfirp  43158  caratheodorylem1  43165  hoicvr  43187  hoidmv1lelem2  43231  hoidmvlelem2  43235  hoiqssbllem2  43262  vonioolem1  43319  vonicclem1  43322  smflimlem4  43407  smfmullem1  43423  iccpartgt  43944  perfectALTVlem2  44240  bgoldbtbndlem2  44324  pgrple2abl  44767  logbpw2m1  44981  dignn0ldlem  45016  2itscp  45195