Theorem lelttrd 11234

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105   class class class wbr 5092  ℝcr 10971   < clt 11110   ≤ cle 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-resscn 11029  ax-pre-lttri 11046  ax-pre-lttrn 11047

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-er 8569  df-en 8805  df-dom 8806  df-sdom 8807  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116

This theorem is referenced by:  lt2msq1  11960  suprzcl  12501  ge0p1rp  12862  elfzolt3  13498  flflp1  13628  ltdifltdiv  13655  modsubdir  13761  seqf1olem1  13863  seqf1olem2  13864  expmulnbnd  14051  discr1  14055  faclbnd5  14113  bcp1nk  14132  hashfun  14252  swrds2  14752  abslt  15125  abs3lem  15149  fzomaxdiflem  15153  icodiamlt  15246  reccn2  15405  o1rlimmul  15427  caucvgrlem  15483  geomulcvg  15687  mertenslem1  15695  bpoly4  15868  ef01bndlem  15992  sin01bnd  15993  cos01bnd  15994  sinltx  15997  eirrlem  16012  rpnnen2lem11  16032  ruclem10  16047  bitsfzolem  16240  bitsfzo  16241  bitsinv1lem  16247  smueqlem  16296  pcfaclem  16696  pockthg  16704  prmreclem5  16718  1arith  16725  4sqlem11  16753  4sqlem12  16754  4sqlem13  16755  coe1tmmul2  21553  ssblex  23687  nlmvscnlem2  23955  nlmvscnlem1  23956  nrginvrcnlem  23961  blcvx  24067  icccmplem2  24092  reconnlem2  24096  metdcnlem  24105  icopnfcnv  24211  nmoleub2lem3  24384  ipcnlem2  24514  ipcnlem1  24515  minveclem3b  24698  minveclem3  24699  pjthlem1  24707  pmltpclem2  24719  ivthlem2  24722  ovollb2lem  24758  iundisj  24818  uniioombllem3  24855  opnmbllem  24871  itg2monolem3  25023  itg2cnlem2  25033  dveflem  25249  dvferm2lem  25256  lhop1lem  25283  dvcnvre  25289  ftc1a  25307  ftc1lem4  25309  coeeulem  25491  dgradd2  25535  aaliou2b  25607  ulmdvlem1  25665  itgulm  25673  radcnvlem1  25678  radcnvlt1  25683  radcnvle  25685  psercnlem1  25690  pserdvlem1  25692  pserdv  25694  abelthlem2  25697  abelthlem7  25703  cosordlem  25792  tanord1  25799  efif1olem1  25804  logcnlem3  25905  logcnlem4  25906  efopnlem1  25917  logtayl  25921  cxpcn3lem  26006  birthdaylem3  26209  efrlim  26225  lgamgulmlem2  26285  lgamucov  26293  ftalem1  26328  ftalem2  26329  ftalem5  26332  basellem1  26336  basellem3  26338  perfectlem2  26484  bposlem1  26538  bposlem3  26540  bposlem6  26543  lgsdirprm  26585  lgsqrlem2  26601  lgseisen  26633  lgsquadlem1  26634  lgsquadlem2  26635  2sqlem8  26680  2sqblem  26685  dchrvmasumiflem1  26755  pntrmax  26818  pntlemc  26849  pntlemg  26852  pntlemr  26856  axpaschlem  27597  axlowdimlem16  27614  clwwisshclwwslem  28666  smcnlem  29347  minvecolem3  29526  pjhthlem1  30041  nmcexi  30676  iundisjf  31215  iundisjfi  31404  psgnfzto1stlem  31654  dya2icoseg  32544  reprgt  32901  hgt750lem  32931  tgoldbachgtde  32940  subfaclim  33449  bcprod  33994  dnicn  34768  unbdqndv2lem1  34785  unbdqndv2lem2  34786  knoppndvlem18  34805  poimirlem6  35888  poimirlem7  35889  poimirlem12  35894  poimirlem15  35897  poimirlem17  35899  poimirlem19  35901  poimirlem20  35902  poimirlem23  35905  poimirlem24  35906  opnmbllem0  35918  mblfinlem3  35921  mblfinlem4  35922  ftc1cnnclem  35953  ftc1anclem7  35961  isbnd3  36047  cntotbnd  36059  rrnequiv  36098  aks4d1p1p3  40331  aks4d1p1p2  40332  aks4d1p1p4  40333  aks4d1p1p7  40336  aks4d1p1p5  40337  aks4d1p5  40342  2np3bcnp1  40357  sticksstones10  40368  sticksstones12a  40370  sticksstones22  40381  metakunt1  40382  metakunt12  40393  metakunt28  40409  metakunt30  40411  flt4lem7  40758  fltnltalem  40761  fltnlta  40762  irrapxlem1  40906  pell14qrgapw  40960  monotoddzzfi  41027  ltrmynn0  41033  jm2.24nn  41044  acongeq  41068  jm2.26lem3  41086  jm3.1lem2  41103  binomcxplemnotnn0  42295  isosctrlem1ALT  42875  rfcnnnub  42900  zltlesub  43159  monoords  43171  supxrge  43212  infleinflem2  43245  uzubioo  43441  fmul01lt1lem1  43461  fmul01lt1lem2  43462  lptre2pt  43517  addlimc  43525  0ellimcdiv  43526  limclner  43528  climleltrp  43553  limsupubuzlem  43589  limsup10exlem  43649  icccncfext  43764  ioodvbdlimc1lem1  43808  ioodvbdlimc1lem2  43809  ioodvbdlimc2lem  43811  dvnmul  43820  iblspltprt  43850  itgspltprt  43856  stoweidlem5  43882  stoweidlem11  43888  stoweidlem13  43890  stoweidlem14  43891  stoweidlem25  43902  stoweidlem26  43903  stoweidlem42  43919  stoweidlem59  43936  stoweid  43940  wallispilem3  43944  wallispilem4  43945  wallispilem5  43946  fourierdlem10  43994  fourierdlem11  43995  fourierdlem12  43996  fourierdlem15  43999  fourierdlem20  44004  fourierdlem24  44008  fourierdlem30  44014  fourierdlem31  44015  fourierdlem33  44017  fourierdlem40  44024  fourierdlem41  44025  fourierdlem42  44026  fourierdlem43  44027  fourierdlem44  44028  fourierdlem46  44029  fourierdlem47  44030  fourierdlem48  44031  fourierdlem50  44033  fourierdlem63  44046  fourierdlem64  44047  fourierdlem65  44048  fourierdlem73  44056  fourierdlem74  44057  fourierdlem75  44058  fourierdlem76  44059  fourierdlem77  44060  fourierdlem78  44061  fourierdlem79  44062  fourierdlem87  44070  fourierdlem91  44074  fourierdlem92  44075  fourierdlem103  44086  fourierdlem104  44087  fouriersw  44108  etransclem19  44130  etransclem23  44134  etransclem48  44159  ioorrnopnlem  44181  iundjiun  44335  omeiunltfirp  44394  caratheodorylem1  44401  hoicvr  44423  hoidmv1lelem2  44467  hoidmvlelem2  44471  hoiqssbllem2  44498  vonioolem1  44555  vonicclem1  44558  smflimlem4  44649  smfmullem1  44666  iccpartgt  45230  perfectALTVlem2  45525  bgoldbtbndlem2  45609  pgrple2abl  46052  logbpw2m1  46264  dignn0ldlem  46299  2itscp  46478