Theorem lelttrd 11296

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   class class class wbr 5073  ℝcr 11029   < clt 11171   ≤ cle 11172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-resscn 11087  ax-pre-lttri 11104  ax-pre-lttrn 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11173  df-mnf 11174  df-xr 11175  df-ltxr 11176  df-le 11177

This theorem is referenced by:  lt2msq1  12032  suprzcl  12601  ge0p1rp  12967  elfzolt3  13616  flflp1  13758  ltdifltdiv  13785  modsubdir  13894  seqf1olem1  13995  seqf1olem2  13996  expmulnbnd  14189  discr1  14193  faclbnd5  14252  bcp1nk  14271  hashfun  14391  swrds2  14894  abslt  15269  abs3lem  15293  fzomaxdiflem  15297  icodiamlt  15392  reccn2  15551  o1rlimmul  15573  caucvgrlem  15627  geomulcvg  15833  mertenslem1  15841  bpoly4  16016  ef01bndlem  16143  sin01bnd  16144  cos01bnd  16145  sinltx  16148  eirrlem  16163  rpnnen2lem11  16183  ruclem10  16198  bitsfzolem  16395  bitsfzo  16396  bitsinv1lem  16402  smueqlem  16451  pcfaclem  16861  pockthg  16869  prmreclem5  16883  1arith  16890  4sqlem11  16918  4sqlem12  16919  4sqlem13  16920  coe1tmmul2  22263  ssblex  24412  nlmvscnlem2  24669  nlmvscnlem1  24670  nrginvrcnlem  24675  blcvx  24782  icccmplem2  24808  reconnlem2  24812  metdcnlem  24821  icopnfcnv  24928  nmoleub2lem3  25101  ipcnlem2  25230  ipcnlem1  25231  minveclem3b  25414  minveclem3  25415  pjthlem1  25423  pmltpclem2  25435  ivthlem2  25438  ovollb2lem  25474  iundisj  25534  uniioombllem3  25571  opnmbllem  25587  itg2monolem3  25738  itg2cnlem2  25748  dveflem  25965  dvferm2lem  25972  lhop1lem  25999  dvcnvre  26005  ftc1a  26023  ftc1lem4  26025  coeeulem  26208  dgradd2  26252  aaliou2b  26326  ulmdvlem1  26384  itgulm  26392  radcnvlem1  26397  radcnvlt1  26402  radcnvle  26404  psercnlem1  26409  pserdvlem1  26411  pserdv  26413  abelthlem2  26416  abelthlem7  26422  cosordlem  26513  tanord1  26520  efif1olem1  26525  logcnlem3  26627  logcnlem4  26628  efopnlem1  26639  logtayl  26643  cxpcn3lem  26730  birthdaylem3  26936  efrlim  26952  lgamgulmlem2  27012  lgamucov  27020  ftalem1  27055  ftalem2  27056  ftalem5  27059  basellem1  27063  basellem3  27065  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  29028  axlowdimlem16  29045  clwwisshclwwslem  30103  smcnlem  30787  minvecolem3  30966  pjhthlem1  31481  nmcexi  32116  iundisjf  32679  iundisjfi  32889  psgnfzto1stlem  33182  esplyfval2  33758  esplyfval3  33765  cos9thpiminplylem1  33975  dya2icoseg  34470  reprgt  34814  hgt750lem  34844  tgoldbachgtde  34853  subfaclim  35425  bcprod  35975  dnicn  36807  unbdqndv2lem1  36824  unbdqndv2lem2  36825  knoppndvlem18  36844  poimirlem6  38002  poimirlem7  38003  poimirlem12  38008  poimirlem15  38011  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem23  38019  poimirlem24  38020  opnmbllem0  38032  mblfinlem3  38035  mblfinlem4  38036  ftc1cnnclem  38067  ftc1anclem7  38075  isbnd3  38160  cntotbnd  38172  rrnequiv  38211  aks4d1p1p3  42563  aks4d1p1p2  42564  aks4d1p1p4  42565  aks4d1p1p7  42568  aks4d1p1p5  42569  aks4d1p5  42574  posbezout  42594  primrootlekpowne0  42599  aks6d1c5lem1  42630  2np3bcnp1  42638  sticksstones10  42649  sticksstones12a  42651  sticksstones22  42662  aks6d1c7lem1  42674  unitscyglem2  42690  flt4lem7  43118  fltnltalem  43121  fltnlta  43122  irrapxlem1  43276  pell14qrgapw  43330  monotoddzzfi  43396  ltrmynn0  43402  jm2.24nn  43413  acongeq  43437  jm2.26lem3  43455  jm3.1lem2  43472  binomcxplemnotnn0  44809  isosctrlem1ALT  45386  rfcnnnub  45493  zltlesub  45741  monoords  45753  supxrge  45791  infleinflem2  45823  uzubioo  46018  fmul01lt1lem1  46037  fmul01lt1lem2  46038  lptre2pt  46091  addlimc  46099  0ellimcdiv  46100  limclner  46102  climleltrp  46127  limsupubuzlem  46163  limsup10exlem  46223  icccncfext  46338  ioodvbdlimc1lem1  46382  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  dvnmul  46394  iblspltprt  46424  itgspltprt  46430  stoweidlem5  46456  stoweidlem11  46462  stoweidlem13  46464  stoweidlem14  46465  stoweidlem25  46476  stoweidlem26  46477  stoweidlem42  46493  stoweidlem59  46510  stoweid  46514  wallispilem3  46518  wallispilem4  46519  wallispilem5  46520  fourierdlem10  46568  fourierdlem11  46569  fourierdlem12  46570  fourierdlem15  46573  fourierdlem20  46578  fourierdlem24  46582  fourierdlem30  46588  fourierdlem31  46589  fourierdlem33  46591  fourierdlem40  46598  fourierdlem41  46599  fourierdlem42  46600  fourierdlem43  46601  fourierdlem44  46602  fourierdlem46  46603  fourierdlem47  46604  fourierdlem48  46605  fourierdlem50  46607  fourierdlem63  46620  fourierdlem64  46621  fourierdlem65  46622  fourierdlem73  46630  fourierdlem74  46631  fourierdlem75  46632  fourierdlem76  46633  fourierdlem77  46634  fourierdlem78  46635  fourierdlem79  46636  fourierdlem87  46644  fourierdlem91  46648  fourierdlem92  46649  fourierdlem103  46660  fourierdlem104  46661  fouriersw  46682  etransclem19  46704  etransclem23  46708  etransclem48  46733  ioorrnopnlem  46755  iundjiun  46911  omeiunltfirp  46970  caratheodorylem1  46977  hoicvr  46999  hoidmv1lelem2  47043  hoidmvlelem2  47047  hoiqssbllem2  47074  vonioolem1  47131  vonicclem1  47134  smflimlem4  47225  smfmullem1  47242  2tceilhalfelfzo1  47807  addmodne  47821  2timesltsqm1  47850  iccpartgt  47910  perfectALTVlem2  48221  bgoldbtbndlem2  48305  pgrple2abl  48864  logbpw2m1  49066  dignn0ldlem  49101  2itscp  49280