Theorem lelttrd 11303

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  lt2msq1  12038  suprzcl  12584  ge0p1rp  12950  elfzolt3  13597  flflp1  13739  ltdifltdiv  13766  modsubdir  13875  seqf1olem1  13976  seqf1olem2  13977  expmulnbnd  14170  discr1  14174  faclbnd5  14233  bcp1nk  14252  hashfun  14372  swrds2  14875  abslt  15250  abs3lem  15274  fzomaxdiflem  15278  icodiamlt  15373  reccn2  15532  o1rlimmul  15554  caucvgrlem  15608  geomulcvg  15811  mertenslem1  15819  bpoly4  15994  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  sinltx  16126  eirrlem  16141  rpnnen2lem11  16161  ruclem10  16176  bitsfzolem  16373  bitsfzo  16374  bitsinv1lem  16380  smueqlem  16429  pcfaclem  16838  pockthg  16846  prmreclem5  16860  1arith  16867  4sqlem11  16895  4sqlem12  16896  4sqlem13  16897  coe1tmmul2  22233  ssblex  24387  nlmvscnlem2  24644  nlmvscnlem1  24645  nrginvrcnlem  24650  blcvx  24757  icccmplem2  24783  reconnlem2  24787  metdcnlem  24796  icopnfcnv  24911  nmoleub2lem3  25086  ipcnlem2  25215  ipcnlem1  25216  minveclem3b  25399  minveclem3  25400  pjthlem1  25408  pmltpclem2  25421  ivthlem2  25424  ovollb2lem  25460  iundisj  25520  uniioombllem3  25557  opnmbllem  25573  itg2monolem3  25724  itg2cnlem2  25734  dveflem  25954  dvferm2lem  25961  lhop1lem  25989  dvcnvre  25995  ftc1a  26015  ftc1lem4  26017  coeeulem  26200  dgradd2  26245  aaliou2b  26320  ulmdvlem1  26380  itgulm  26388  radcnvlem1  26393  radcnvlt1  26398  radcnvle  26400  psercnlem1  26406  pserdvlem1  26408  pserdv  26410  abelthlem2  26413  abelthlem7  26419  cosordlem  26510  tanord1  26517  efif1olem1  26522  logcnlem3  26624  logcnlem4  26625  efopnlem1  26636  logtayl  26640  cxpcn3lem  26728  birthdaylem3  26934  efrlim  26950  efrlimOLD  26951  lgamgulmlem2  27011  lgamucov  27019  ftalem1  27054  ftalem2  27055  ftalem5  27058  basellem1  27062  basellem3  27064  perfectlem2  27212  bposlem1  27266  bposlem3  27268  bposlem6  27271  lgsdirprm  27313  lgsqrlem2  27329  lgseisen  27361  lgsquadlem1  27362  lgsquadlem2  27363  2sqlem8  27408  2sqblem  27413  dchrvmasumiflem1  27483  pntrmax  27546  pntlemc  27577  pntlemg  27580  pntlemr  27584  axpaschlem  29029  axlowdimlem16  29046  clwwisshclwwslem  30105  smcnlem  30789  minvecolem3  30968  pjhthlem1  31483  nmcexi  32118  iundisjf  32680  iundisjfi  32891  psgnfzto1stlem  33198  esplyfval2  33746  esplyfval3  33753  cos9thpiminplylem1  33964  dya2icoseg  34459  reprgt  34803  hgt750lem  34833  tgoldbachgtde  34842  subfaclim  35408  bcprod  35958  dnicn  36718  unbdqndv2lem1  36735  unbdqndv2lem2  36736  knoppndvlem18  36755  poimirlem6  37881  poimirlem7  37882  poimirlem12  37887  poimirlem15  37890  poimirlem17  37892  poimirlem19  37894  poimirlem20  37895  poimirlem23  37898  poimirlem24  37899  opnmbllem0  37911  mblfinlem3  37914  mblfinlem4  37915  ftc1cnnclem  37946  ftc1anclem7  37954  isbnd3  38039  cntotbnd  38051  rrnequiv  38090  aks4d1p1p3  42443  aks4d1p1p2  42444  aks4d1p1p4  42445  aks4d1p1p7  42448  aks4d1p1p5  42449  aks4d1p5  42454  posbezout  42474  primrootlekpowne0  42479  aks6d1c5lem1  42510  2np3bcnp1  42518  sticksstones10  42529  sticksstones12a  42531  sticksstones22  42542  aks6d1c7lem1  42554  unitscyglem2  42570  flt4lem7  43021  fltnltalem  43024  fltnlta  43025  irrapxlem1  43183  pell14qrgapw  43237  monotoddzzfi  43303  ltrmynn0  43309  jm2.24nn  43320  acongeq  43344  jm2.26lem3  43362  jm3.1lem2  43379  binomcxplemnotnn0  44716  isosctrlem1ALT  45293  rfcnnnub  45400  zltlesub  45651  monoords  45663  supxrge  45701  infleinflem2  45733  uzubioo  45929  fmul01lt1lem1  45948  fmul01lt1lem2  45949  lptre2pt  46002  addlimc  46010  0ellimcdiv  46011  limclner  46013  climleltrp  46038  limsupubuzlem  46074  limsup10exlem  46134  icccncfext  46249  ioodvbdlimc1lem1  46293  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  dvnmul  46305  iblspltprt  46335  itgspltprt  46341  stoweidlem5  46367  stoweidlem11  46373  stoweidlem13  46375  stoweidlem14  46376  stoweidlem25  46387  stoweidlem26  46388  stoweidlem42  46404  stoweidlem59  46421  stoweid  46425  wallispilem3  46429  wallispilem4  46430  wallispilem5  46431  fourierdlem10  46479  fourierdlem11  46480  fourierdlem12  46481  fourierdlem15  46484  fourierdlem20  46489  fourierdlem24  46493  fourierdlem30  46499  fourierdlem31  46500  fourierdlem33  46502  fourierdlem40  46509  fourierdlem41  46510  fourierdlem42  46511  fourierdlem43  46512  fourierdlem44  46513  fourierdlem46  46514  fourierdlem47  46515  fourierdlem48  46516  fourierdlem50  46518  fourierdlem63  46531  fourierdlem64  46532  fourierdlem65  46533  fourierdlem73  46541  fourierdlem74  46542  fourierdlem75  46543  fourierdlem76  46544  fourierdlem77  46545  fourierdlem78  46546  fourierdlem79  46547  fourierdlem87  46555  fourierdlem91  46559  fourierdlem92  46560  fourierdlem103  46571  fourierdlem104  46572  fouriersw  46593  etransclem19  46615  etransclem23  46619  etransclem48  46644  ioorrnopnlem  46666  iundjiun  46822  omeiunltfirp  46881  caratheodorylem1  46888  hoicvr  46910  hoidmv1lelem2  46954  hoidmvlelem2  46958  hoiqssbllem2  46985  vonioolem1  47042  vonicclem1  47045  smflimlem4  47136  smfmullem1  47153  2tceilhalfelfzo1  47696  addmodne  47708  iccpartgt  47791  perfectALTVlem2  48086  bgoldbtbndlem2  48170  pgrple2abl  48729  logbpw2m1  48931  dignn0ldlem  48966  2itscp  49145