Theorem lelttrd 11274

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   < clt 11149   ≤ cle 11150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  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 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155

This theorem is referenced by:  lt2msq1  12009  suprzcl  12556  ge0p1rp  12926  elfzolt3  13572  flflp1  13711  ltdifltdiv  13738  modsubdir  13847  seqf1olem1  13948  seqf1olem2  13949  expmulnbnd  14142  discr1  14146  faclbnd5  14205  bcp1nk  14224  hashfun  14344  swrds2  14847  abslt  15222  abs3lem  15246  fzomaxdiflem  15250  icodiamlt  15345  reccn2  15504  o1rlimmul  15526  caucvgrlem  15580  geomulcvg  15783  mertenslem1  15791  bpoly4  15966  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  sinltx  16098  eirrlem  16113  rpnnen2lem11  16133  ruclem10  16148  bitsfzolem  16345  bitsfzo  16346  bitsinv1lem  16352  smueqlem  16401  pcfaclem  16810  pockthg  16818  prmreclem5  16832  1arith  16839  4sqlem11  16867  4sqlem12  16868  4sqlem13  16869  coe1tmmul2  22160  ssblex  24314  nlmvscnlem2  24571  nlmvscnlem1  24572  nrginvrcnlem  24577  blcvx  24684  icccmplem2  24710  reconnlem2  24714  metdcnlem  24723  icopnfcnv  24838  nmoleub2lem3  25013  ipcnlem2  25142  ipcnlem1  25143  minveclem3b  25326  minveclem3  25327  pjthlem1  25335  pmltpclem2  25348  ivthlem2  25351  ovollb2lem  25387  iundisj  25447  uniioombllem3  25484  opnmbllem  25500  itg2monolem3  25651  itg2cnlem2  25661  dveflem  25881  dvferm2lem  25888  lhop1lem  25916  dvcnvre  25922  ftc1a  25942  ftc1lem4  25944  coeeulem  26127  dgradd2  26172  aaliou2b  26247  ulmdvlem1  26307  itgulm  26315  radcnvlem1  26320  radcnvlt1  26325  radcnvle  26327  psercnlem1  26333  pserdvlem1  26335  pserdv  26337  abelthlem2  26340  abelthlem7  26346  cosordlem  26437  tanord1  26444  efif1olem1  26449  logcnlem3  26551  logcnlem4  26552  efopnlem1  26563  logtayl  26567  cxpcn3lem  26655  birthdaylem3  26861  efrlim  26877  efrlimOLD  26878  lgamgulmlem2  26938  lgamucov  26946  ftalem1  26981  ftalem2  26982  ftalem5  26985  basellem1  26989  basellem3  26991  perfectlem2  27139  bposlem1  27193  bposlem3  27195  bposlem6  27198  lgsdirprm  27240  lgsqrlem2  27256  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  2sqlem8  27335  2sqblem  27340  dchrvmasumiflem1  27410  pntrmax  27473  pntlemc  27504  pntlemg  27507  pntlemr  27511  axpaschlem  28885  axlowdimlem16  28902  clwwisshclwwslem  29958  smcnlem  30641  minvecolem3  30820  pjhthlem1  31335  nmcexi  31970  iundisjf  32533  iundisjfi  32740  psgnfzto1stlem  33043  cos9thpiminplylem1  33755  dya2icoseg  34251  reprgt  34595  hgt750lem  34625  tgoldbachgtde  34634  subfaclim  35171  bcprod  35721  dnicn  36476  unbdqndv2lem1  36493  unbdqndv2lem2  36494  knoppndvlem18  36513  poimirlem6  37616  poimirlem7  37617  poimirlem12  37622  poimirlem15  37625  poimirlem17  37627  poimirlem19  37629  poimirlem20  37630  poimirlem23  37633  poimirlem24  37634  opnmbllem0  37646  mblfinlem3  37649  mblfinlem4  37650  ftc1cnnclem  37681  ftc1anclem7  37689  isbnd3  37774  cntotbnd  37786  rrnequiv  37825  aks4d1p1p3  42052  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p7  42057  aks4d1p1p5  42058  aks4d1p5  42063  posbezout  42083  primrootlekpowne0  42088  aks6d1c5lem1  42119  2np3bcnp1  42127  sticksstones10  42138  sticksstones12a  42140  sticksstones22  42151  aks6d1c7lem1  42163  unitscyglem2  42179  flt4lem7  42642  fltnltalem  42645  fltnlta  42646  irrapxlem1  42805  pell14qrgapw  42859  monotoddzzfi  42925  ltrmynn0  42931  jm2.24nn  42942  acongeq  42966  jm2.26lem3  42984  jm3.1lem2  43001  binomcxplemnotnn0  44339  isosctrlem1ALT  44917  rfcnnnub  45024  zltlesub  45277  monoords  45289  supxrge  45328  infleinflem2  45360  uzubioo  45556  fmul01lt1lem1  45575  fmul01lt1lem2  45576  lptre2pt  45631  addlimc  45639  0ellimcdiv  45640  limclner  45642  climleltrp  45667  limsupubuzlem  45703  limsup10exlem  45763  icccncfext  45878  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  iblspltprt  45964  itgspltprt  45970  stoweidlem5  45996  stoweidlem11  46002  stoweidlem13  46004  stoweidlem14  46005  stoweidlem25  46016  stoweidlem26  46017  stoweidlem42  46033  stoweidlem59  46050  stoweid  46054  wallispilem3  46058  wallispilem4  46059  wallispilem5  46060  fourierdlem10  46108  fourierdlem11  46109  fourierdlem12  46110  fourierdlem15  46113  fourierdlem20  46118  fourierdlem24  46122  fourierdlem30  46128  fourierdlem31  46129  fourierdlem33  46131  fourierdlem40  46138  fourierdlem41  46139  fourierdlem42  46140  fourierdlem43  46141  fourierdlem44  46142  fourierdlem46  46143  fourierdlem47  46144  fourierdlem48  46145  fourierdlem50  46147  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem77  46174  fourierdlem78  46175  fourierdlem79  46176  fourierdlem87  46184  fourierdlem91  46188  fourierdlem92  46189  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem19  46244  etransclem23  46248  etransclem48  46273  ioorrnopnlem  46295  iundjiun  46451  omeiunltfirp  46510  caratheodorylem1  46517  hoicvr  46539  hoidmv1lelem2  46583  hoidmvlelem2  46587  hoiqssbllem2  46614  vonioolem1  46671  vonicclem1  46674  smflimlem4  46765  smfmullem1  46782  2tceilhalfelfzo1  47326  addmodne  47338  iccpartgt  47421  perfectALTVlem2  47716  bgoldbtbndlem2  47800  pgrple2abl  48359  logbpw2m1  48562  dignn0ldlem  48597  2itscp  48776