Theorem lelttrd 11368

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   class class class wbr 5113  ℝcr 11099   < clt 11243   ≤ cle 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-pre-lttri 11174  ax-pre-lttrn 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249

This theorem is referenced by:  lt2msq1  12099  suprzcl  12676  ge0p1rp  13049  elfzolt3  13698  flflp1  13840  ltdifltdiv  13867  modsubdir  13976  seqf1olem1  14077  seqf1olem2  14078  expmulnbnd  14271  discr1  14275  faclbnd5  14334  bcp1nk  14353  hashfun  14474  swrds2  14977  abslt  15366  abs3lem  15390  fzomaxdiflem  15394  icodiamlt  15489  reccn2  15648  o1rlimmul  15670  caucvgrlem  15724  geomulcvg  15930  mertenslem1  15938  bpoly4  16113  ef01bndlem  16240  sin01bnd  16241  cos01bnd  16242  sinltx  16245  eirrlem  16260  rpnnen2lem11  16280  ruclem10  16295  bitsfzolem  16492  bitsfzo  16493  bitsinv1lem  16499  smueqlem  16548  pcfaclem  16958  pockthg  16966  prmreclem5  16980  1arith  16987  4sqlem11  17015  4sqlem12  17016  4sqlem13  17017  coe1tmmul2  22406  ssblex  24554  nlmvscnlem2  24811  nlmvscnlem1  24812  nrginvrcnlem  24817  blcvx  24924  icccmplem2  24950  reconnlem2  24954  metdcnlem  24963  icopnfcnv  25070  nmoleub2lem3  25243  ipcnlem2  25372  ipcnlem1  25373  minveclem3b  25556  minveclem3  25557  pjthlem1  25565  pmltpclem2  25577  ivthlem2  25580  ovollb2lem  25616  iundisj  25676  uniioombllem3  25713  opnmbllem  25729  itg2monolem3  25880  itg2cnlem2  25890  dveflem  26107  dvferm2lem  26114  lhop1lem  26141  dvcnvre  26147  ftc1a  26165  ftc1lem4  26167  coeeulem  26350  dgradd2  26394  aaliou2b  26471  ulmdvlem1  26529  itgulm  26537  radcnvlem1  26542  radcnvlt1  26547  radcnvle  26549  psercnlem1  26554  pserdvlem1  26556  pserdv  26558  abelthlem2  26561  abelthlem7  26567  cosordlem  26661  tanord1  26668  efif1olem1  26673  logcnlem3  26775  logcnlem4  26776  efopnlem1  26787  logtayl  26791  cxpcn3lem  26878  birthdaylem3  27084  efrlim  27100  lgamgulmlem2  27160  lgamucov  27168  ftalem1  27203  ftalem2  27204  ftalem5  27207  basellem1  27211  basellem3  27213  perfectlem2  27360  bposlem1  27414  bposlem3  27416  bposlem6  27419  lgsdirprm  27461  lgsqrlem2  27477  lgseisen  27509  lgsquadlem1  27510  lgsquadlem2  27511  2sqlem8  27556  2sqblem  27561  dchrvmasumiflem1  27631  pntrmax  27694  pntlemc  27725  pntlemg  27728  pntlemr  27732  axpaschlem  29231  axlowdimlem16  29248  clwwisshclwwslem  30306  smcnlem  30990  minvecolem3  31169  pjhthlem1  31684  nmcexi  32319  iundisjf  32875  iundisjfi  33082  psgnfzto1stlem  33361  esplyfval2  33900  esplyfval3  33907  cos9thpiminplylem1  34117  dya2icoseg  34612  reprgt  34953  hgt750lem  34983  tgoldbachgtde  34992  subfaclim  35613  bcprod  36163  dnicn  37004  unbdqndv2lem1  37021  unbdqndv2lem2  37022  knoppndvlem18  37041  poimirlem6  38199  poimirlem7  38200  poimirlem12  38205  poimirlem15  38208  poimirlem17  38210  poimirlem19  38212  poimirlem20  38213  poimirlem23  38216  poimirlem24  38217  opnmbllem0  38229  mblfinlem3  38232  mblfinlem4  38233  ftc1cnnclem  38264  ftc1anclem7  38272  isbnd3  38357  cntotbnd  38369  rrnequiv  38408  aks4d1p1p3  42760  aks4d1p1p2  42761  aks4d1p1p4  42762  aks4d1p1p7  42765  aks4d1p1p5  42766  aks4d1p5  42771  posbezout  42791  primrootlekpowne0  42796  aks6d1c5lem1  42827  2np3bcnp1  42835  sticksstones10  42846  sticksstones12a  42848  sticksstones22  42859  aks6d1c7lem1  42871  unitscyglem2  42887  flt4lem7  43317  fltnltalem  43320  fltnlta  43321  irrapxlem1  43475  pell14qrgapw  43529  monotoddzzfi  43595  ltrmynn0  43601  jm2.24nn  43612  acongeq  43636  jm2.26lem3  43654  jm3.1lem2  43671  binomcxplemnotnn0  44992  isosctrlem1ALT  45568  rfcnnnub  45682  zltlesub  45930  monoords  45942  supxrge  45980  infleinflem2  46012  uzubioo  46207  fmul01lt1lem1  46226  fmul01lt1lem2  46227  lptre2pt  46280  addlimc  46288  0ellimcdiv  46289  limclner  46291  climleltrp  46316  limsupubuzlem  46352  limsup10exlem  46412  icccncfext  46527  ioodvbdlimc1lem1  46571  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  dvnmul  46583  iblspltprt  46613  itgspltprt  46619  stoweidlem5  46645  stoweidlem11  46651  stoweidlem13  46653  stoweidlem14  46654  stoweidlem25  46665  stoweidlem26  46666  stoweidlem42  46682  stoweidlem59  46699  stoweid  46703  wallispilem3  46707  wallispilem4  46708  wallispilem5  46709  fourierdlem10  46757  fourierdlem11  46758  fourierdlem12  46759  fourierdlem15  46762  fourierdlem20  46767  fourierdlem24  46771  fourierdlem30  46777  fourierdlem31  46778  fourierdlem33  46780  fourierdlem40  46787  fourierdlem41  46788  fourierdlem42  46789  fourierdlem43  46790  fourierdlem44  46791  fourierdlem46  46792  fourierdlem47  46793  fourierdlem48  46794  fourierdlem50  46796  fourierdlem63  46809  fourierdlem64  46810  fourierdlem65  46811  fourierdlem73  46819  fourierdlem74  46820  fourierdlem75  46821  fourierdlem76  46822  fourierdlem77  46823  fourierdlem78  46824  fourierdlem79  46825  fourierdlem87  46833  fourierdlem91  46837  fourierdlem92  46838  fourierdlem103  46849  fourierdlem104  46850  fouriersw  46871  etransclem19  46893  etransclem23  46897  etransclem48  46922  ioorrnopnlem  46944  iundjiun  47100  omeiunltfirp  47159  caratheodorylem1  47166  hoicvr  47188  hoidmv1lelem2  47232  hoidmvlelem2  47236  hoiqssbllem2  47263  vonioolem1  47320  vonicclem1  47323  smflimlem4  47414  smfmullem1  47431  2tceilhalfelfzo1  47996  addmodne  48010  2timesltsqm1  48039  iccpartgt  48099  perfectALTVlem2  48410  bgoldbtbndlem2  48494  pgrple2abl  49064  logbpw2m1  49266  dignn0ldlem  49301  2itscp  49480