Theorem lelttrd 11271

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005   < clt 11146   ≤ cle 11147

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152

This theorem is referenced by:  lt2msq1  12006  suprzcl  12553  ge0p1rp  12923  elfzolt3  13569  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  22190  ssblex  24343  nlmvscnlem2  24600  nlmvscnlem1  24601  nrginvrcnlem  24606  blcvx  24713  icccmplem2  24739  reconnlem2  24743  metdcnlem  24752  icopnfcnv  24867  nmoleub2lem3  25042  ipcnlem2  25171  ipcnlem1  25172  minveclem3b  25355  minveclem3  25356  pjthlem1  25364  pmltpclem2  25377  ivthlem2  25380  ovollb2lem  25416  iundisj  25476  uniioombllem3  25513  opnmbllem  25529  itg2monolem3  25680  itg2cnlem2  25690  dveflem  25910  dvferm2lem  25917  lhop1lem  25945  dvcnvre  25951  ftc1a  25971  ftc1lem4  25973  coeeulem  26156  dgradd2  26201  aaliou2b  26276  ulmdvlem1  26336  itgulm  26344  radcnvlem1  26349  radcnvlt1  26354  radcnvle  26356  psercnlem1  26362  pserdvlem1  26364  pserdv  26366  abelthlem2  26369  abelthlem7  26375  cosordlem  26466  tanord1  26473  efif1olem1  26478  logcnlem3  26580  logcnlem4  26581  efopnlem1  26592  logtayl  26596  cxpcn3lem  26684  birthdaylem3  26890  efrlim  26906  efrlimOLD  26907  lgamgulmlem2  26967  lgamucov  26975  ftalem1  27010  ftalem2  27011  ftalem5  27014  basellem1  27018  basellem3  27020  perfectlem2  27168  bposlem1  27222  bposlem3  27224  bposlem6  27227  lgsdirprm  27269  lgsqrlem2  27285  lgseisen  27317  lgsquadlem1  27318  lgsquadlem2  27319  2sqlem8  27364  2sqblem  27369  dchrvmasumiflem1  27439  pntrmax  27502  pntlemc  27533  pntlemg  27536  pntlemr  27540  axpaschlem  28918  axlowdimlem16  28935  clwwisshclwwslem  29994  smcnlem  30677  minvecolem3  30856  pjhthlem1  31371  nmcexi  32006  iundisjf  32569  iundisjfi  32778  psgnfzto1stlem  33069  cos9thpiminplylem1  33795  dya2icoseg  34290  reprgt  34634  hgt750lem  34664  tgoldbachgtde  34673  subfaclim  35232  bcprod  35782  dnicn  36536  unbdqndv2lem1  36553  unbdqndv2lem2  36554  knoppndvlem18  36573  poimirlem6  37676  poimirlem7  37677  poimirlem12  37682  poimirlem15  37685  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  poimirlem24  37694  opnmbllem0  37706  mblfinlem3  37709  mblfinlem4  37710  ftc1cnnclem  37741  ftc1anclem7  37749  isbnd3  37834  cntotbnd  37846  rrnequiv  37885  aks4d1p1p3  42172  aks4d1p1p2  42173  aks4d1p1p4  42174  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p5  42183  posbezout  42203  primrootlekpowne0  42208  aks6d1c5lem1  42239  2np3bcnp1  42247  sticksstones10  42258  sticksstones12a  42260  sticksstones22  42271  aks6d1c7lem1  42283  unitscyglem2  42299  flt4lem7  42762  fltnltalem  42765  fltnlta  42766  irrapxlem1  42925  pell14qrgapw  42979  monotoddzzfi  43045  ltrmynn0  43051  jm2.24nn  43062  acongeq  43086  jm2.26lem3  43104  jm3.1lem2  43121  binomcxplemnotnn0  44459  isosctrlem1ALT  45036  rfcnnnub  45143  zltlesub  45396  monoords  45408  supxrge  45447  infleinflem2  45479  uzubioo  45675  fmul01lt1lem1  45694  fmul01lt1lem2  45695  lptre2pt  45748  addlimc  45756  0ellimcdiv  45757  limclner  45759  climleltrp  45784  limsupubuzlem  45820  limsup10exlem  45880  icccncfext  45995  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnmul  46051  iblspltprt  46081  itgspltprt  46087  stoweidlem5  46113  stoweidlem11  46119  stoweidlem13  46121  stoweidlem14  46122  stoweidlem25  46133  stoweidlem26  46134  stoweidlem42  46150  stoweidlem59  46167  stoweid  46171  wallispilem3  46175  wallispilem4  46176  wallispilem5  46177  fourierdlem10  46225  fourierdlem11  46226  fourierdlem12  46227  fourierdlem15  46230  fourierdlem20  46235  fourierdlem24  46239  fourierdlem30  46245  fourierdlem31  46246  fourierdlem33  46248  fourierdlem40  46255  fourierdlem41  46256  fourierdlem42  46257  fourierdlem43  46258  fourierdlem44  46259  fourierdlem46  46260  fourierdlem47  46261  fourierdlem48  46262  fourierdlem50  46264  fourierdlem63  46277  fourierdlem64  46278  fourierdlem65  46279  fourierdlem73  46287  fourierdlem74  46288  fourierdlem75  46289  fourierdlem76  46290  fourierdlem77  46291  fourierdlem78  46292  fourierdlem79  46293  fourierdlem87  46301  fourierdlem91  46305  fourierdlem92  46306  fourierdlem103  46317  fourierdlem104  46318  fouriersw  46339  etransclem19  46361  etransclem23  46365  etransclem48  46390  ioorrnopnlem  46412  iundjiun  46568  omeiunltfirp  46627  caratheodorylem1  46634  hoicvr  46656  hoidmv1lelem2  46700  hoidmvlelem2  46704  hoiqssbllem2  46731  vonioolem1  46788  vonicclem1  46791  smflimlem4  46882  smfmullem1  46899  2tceilhalfelfzo1  47442  addmodne  47454  iccpartgt  47537  perfectALTVlem2  47832  bgoldbtbndlem2  47916  pgrple2abl  48475  logbpw2m1  48678  dignn0ldlem  48713  2itscp  48892