Theorem lelttrd 11063

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946

This theorem is referenced by:  lt2msq1  11789  suprzcl  12330  ge0p1rp  12690  elfzolt3  13326  flflp1  13455  ltdifltdiv  13482  modsubdir  13588  seqf1olem1  13690  seqf1olem2  13691  expmulnbnd  13878  discr1  13882  faclbnd5  13940  bcp1nk  13959  hashfun  14080  swrds2  14581  abslt  14954  abs3lem  14978  fzomaxdiflem  14982  icodiamlt  15075  reccn2  15234  o1rlimmul  15256  caucvgrlem  15312  geomulcvg  15516  mertenslem1  15524  bpoly4  15697  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  sinltx  15826  eirrlem  15841  rpnnen2lem11  15861  ruclem10  15876  bitsfzolem  16069  bitsfzo  16070  bitsinv1lem  16076  smueqlem  16125  pcfaclem  16527  pockthg  16535  prmreclem5  16549  1arith  16556  4sqlem11  16584  4sqlem12  16585  4sqlem13  16586  coe1tmmul2  21357  ssblex  23489  nlmvscnlem2  23755  nlmvscnlem1  23756  nrginvrcnlem  23761  blcvx  23867  icccmplem2  23892  reconnlem2  23896  metdcnlem  23905  icopnfcnv  24011  nmoleub2lem3  24184  ipcnlem2  24313  ipcnlem1  24314  minveclem3b  24497  minveclem3  24498  pjthlem1  24506  pmltpclem2  24518  ivthlem2  24521  ovollb2lem  24557  iundisj  24617  uniioombllem3  24654  opnmbllem  24670  itg2monolem3  24822  itg2cnlem2  24832  dveflem  25048  dvferm2lem  25055  lhop1lem  25082  dvcnvre  25088  ftc1a  25106  ftc1lem4  25108  coeeulem  25290  dgradd2  25334  aaliou2b  25406  ulmdvlem1  25464  itgulm  25472  radcnvlem1  25477  radcnvlt1  25482  radcnvle  25484  psercnlem1  25489  pserdvlem1  25491  pserdv  25493  abelthlem2  25496  abelthlem7  25502  cosordlem  25591  tanord1  25598  efif1olem1  25603  logcnlem3  25704  logcnlem4  25705  efopnlem1  25716  logtayl  25720  cxpcn3lem  25805  birthdaylem3  26008  efrlim  26024  lgamgulmlem2  26084  lgamucov  26092  ftalem1  26127  ftalem2  26128  ftalem5  26131  basellem1  26135  basellem3  26137  perfectlem2  26283  bposlem1  26337  bposlem3  26339  bposlem6  26342  lgsdirprm  26384  lgsqrlem2  26400  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  2sqlem8  26479  2sqblem  26484  dchrvmasumiflem1  26554  pntrmax  26617  pntlemc  26648  pntlemg  26651  pntlemr  26655  axpaschlem  27211  axlowdimlem16  27228  clwwisshclwwslem  28279  smcnlem  28960  minvecolem3  29139  pjhthlem1  29654  nmcexi  30289  iundisjf  30829  iundisjfi  31019  psgnfzto1stlem  31269  dya2icoseg  32144  reprgt  32501  hgt750lem  32531  tgoldbachgtde  32540  subfaclim  33050  bcprod  33610  dnicn  34599  unbdqndv2lem1  34616  unbdqndv2lem2  34617  knoppndvlem18  34636  poimirlem6  35710  poimirlem7  35711  poimirlem12  35716  poimirlem15  35719  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  opnmbllem0  35740  mblfinlem3  35743  mblfinlem4  35744  ftc1cnnclem  35775  ftc1anclem7  35783  isbnd3  35869  cntotbnd  35881  rrnequiv  35920  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p5  40016  2np3bcnp1  40028  sticksstones10  40039  sticksstones12a  40041  sticksstones22  40052  metakunt1  40053  metakunt12  40064  metakunt28  40080  metakunt30  40082  flt4lem7  40412  fltnltalem  40415  fltnlta  40416  irrapxlem1  40560  pell14qrgapw  40614  monotoddzzfi  40680  ltrmynn0  40686  jm2.24nn  40697  acongeq  40721  jm2.26lem3  40739  jm3.1lem2  40756  binomcxplemnotnn0  41863  isosctrlem1ALT  42443  rfcnnnub  42468  zltlesub  42713  monoords  42726  supxrge  42767  infleinflem2  42800  uzubioo  42995  fmul01lt1lem1  43015  fmul01lt1lem2  43016  lptre2pt  43071  addlimc  43079  0ellimcdiv  43080  limclner  43082  climleltrp  43107  limsupubuzlem  43143  limsup10exlem  43203  icccncfext  43318  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  iblspltprt  43404  itgspltprt  43410  stoweidlem5  43436  stoweidlem11  43442  stoweidlem13  43444  stoweidlem14  43445  stoweidlem25  43456  stoweidlem26  43457  stoweidlem42  43473  stoweidlem59  43490  stoweid  43494  wallispilem3  43498  wallispilem4  43499  wallispilem5  43500  fourierdlem10  43548  fourierdlem11  43549  fourierdlem12  43550  fourierdlem15  43553  fourierdlem20  43558  fourierdlem24  43562  fourierdlem30  43568  fourierdlem31  43569  fourierdlem33  43571  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem43  43581  fourierdlem44  43582  fourierdlem46  43583  fourierdlem47  43584  fourierdlem48  43585  fourierdlem50  43587  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem77  43614  fourierdlem78  43615  fourierdlem79  43616  fourierdlem87  43624  fourierdlem91  43628  fourierdlem92  43629  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  etransclem19  43684  etransclem23  43688  etransclem48  43713  ioorrnopnlem  43735  iundjiun  43888  omeiunltfirp  43947  caratheodorylem1  43954  hoicvr  43976  hoidmv1lelem2  44020  hoidmvlelem2  44024  hoiqssbllem2  44051  vonioolem1  44108  vonicclem1  44111  smflimlem4  44196  smfmullem1  44212  iccpartgt  44767  perfectALTVlem2  45062  bgoldbtbndlem2  45146  pgrple2abl  45589  logbpw2m1  45801  dignn0ldlem  45836  2itscp  46015