MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lelttrd Structured version   Visualization version   GIF version

Theorem lelttrd 10798
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
StepHypRef Expression
1 lelttrd.4 . 2 (𝜑𝐴𝐵)
2 lelttrd.5 . 2 (𝜑𝐵 < 𝐶)
3 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
4 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
5 letrd.3 . . 3 (𝜑𝐶 ∈ ℝ)
6 lelttr 10731 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1368 . 2 (𝜑 → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 698 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115   class class class wbr 5053  cr 10536   < clt 10675  cle 10676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681
This theorem is referenced by:  lt2msq1  11524  suprzcl  12061  ge0p1rp  12419  elfzolt3  13054  flflp1  13183  ltdifltdiv  13210  modsubdir  13314  seqf1olem1  13416  seqf1olem2  13417  expmulnbnd  13603  discr1  13607  faclbnd5  13665  bcp1nk  13684  hashfun  13805  swrds2  14304  abslt  14676  abs3lem  14700  fzomaxdiflem  14704  icodiamlt  14797  reccn2  14955  o1rlimmul  14977  caucvgrlem  15031  geomulcvg  15234  mertenslem1  15242  bpoly4  15415  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  sinltx  15544  eirrlem  15559  rpnnen2lem11  15579  ruclem10  15594  bitsfzolem  15783  bitsfzo  15784  bitsinv1lem  15790  smueqlem  15839  pcfaclem  16234  pockthg  16242  prmreclem5  16256  1arith  16263  4sqlem11  16291  4sqlem12  16292  4sqlem13  16293  coe1tmmul2  20914  ssblex  23044  nlmvscnlem2  23300  nlmvscnlem1  23301  nrginvrcnlem  23306  blcvx  23412  icccmplem2  23437  reconnlem2  23441  metdcnlem  23450  icopnfcnv  23556  nmoleub2lem3  23729  ipcnlem2  23857  ipcnlem1  23858  minveclem3b  24041  minveclem3  24042  pjthlem1  24050  pmltpclem2  24062  ivthlem2  24065  ovollb2lem  24101  iundisj  24161  uniioombllem3  24198  opnmbllem  24214  itg2monolem3  24365  itg2cnlem2  24375  dveflem  24591  dvferm2lem  24598  lhop1lem  24625  dvcnvre  24631  ftc1a  24649  ftc1lem4  24651  coeeulem  24830  dgradd2  24874  aaliou2b  24946  ulmdvlem1  25004  itgulm  25012  radcnvlem1  25017  radcnvlt1  25022  radcnvle  25024  psercnlem1  25029  pserdvlem1  25031  pserdv  25033  abelthlem2  25036  abelthlem7  25042  cosordlem  25131  tanord1  25138  efif1olem1  25143  logcnlem3  25244  logcnlem4  25245  efopnlem1  25256  logtayl  25260  cxpcn3lem  25345  birthdaylem3  25548  efrlim  25564  lgamgulmlem2  25624  lgamucov  25632  ftalem1  25667  ftalem2  25668  ftalem5  25671  basellem1  25675  basellem3  25677  perfectlem2  25823  bposlem1  25877  bposlem3  25879  bposlem6  25882  lgsdirprm  25924  lgsqrlem2  25940  lgseisen  25972  lgsquadlem1  25973  lgsquadlem2  25974  2sqlem8  26019  2sqblem  26024  dchrvmasumiflem1  26094  pntrmax  26157  pntlemc  26188  pntlemg  26191  pntlemr  26195  axpaschlem  26743  axlowdimlem16  26760  clwwisshclwwslem  27808  smcnlem  28489  minvecolem3  28668  pjhthlem1  29183  nmcexi  29818  iundisjf  30358  iundisjfi  30540  psgnfzto1stlem  30784  dya2icoseg  31620  reprgt  31977  hgt750lem  32007  tgoldbachgtde  32016  subfaclim  32520  bcprod  33055  dnicn  33916  unbdqndv2lem1  33933  unbdqndv2lem2  33934  knoppndvlem18  33953  poimirlem6  35035  poimirlem7  35036  poimirlem12  35041  poimirlem15  35044  poimirlem17  35046  poimirlem19  35048  poimirlem20  35049  poimirlem23  35052  poimirlem24  35053  opnmbllem0  35065  mblfinlem3  35068  mblfinlem4  35069  ftc1cnnclem  35100  ftc1anclem7  35108  isbnd3  35194  cntotbnd  35206  rrnequiv  35245  2np3bcnp1  39321  metakunt1  39323  metakunt12  39334  fltnltalem  39562  fltnlta  39563  irrapxlem1  39707  pell14qrgapw  39761  monotoddzzfi  39827  ltrmynn0  39833  jm2.24nn  39844  acongeq  39868  jm2.26lem3  39886  jm3.1lem2  39903  binomcxplemnotnn0  41008  isosctrlem1ALT  41588  rfcnnnub  41613  zltlesub  41869  monoords  41882  supxrge  41923  infleinflem2  41956  uzubioo  42157  fmul01lt1lem1  42179  fmul01lt1lem2  42180  lptre2pt  42235  addlimc  42243  0ellimcdiv  42244  limclner  42246  climleltrp  42271  limsupubuzlem  42307  limsup10exlem  42367  icccncfext  42482  ioodvbdlimc1lem1  42526  ioodvbdlimc1lem2  42527  ioodvbdlimc2lem  42529  dvnmul  42538  iblspltprt  42568  itgspltprt  42574  stoweidlem5  42600  stoweidlem11  42606  stoweidlem13  42608  stoweidlem14  42609  stoweidlem25  42620  stoweidlem26  42621  stoweidlem42  42637  stoweidlem59  42654  stoweid  42658  wallispilem3  42662  wallispilem4  42663  wallispilem5  42664  fourierdlem10  42712  fourierdlem11  42713  fourierdlem12  42714  fourierdlem15  42717  fourierdlem20  42722  fourierdlem24  42726  fourierdlem30  42732  fourierdlem31  42733  fourierdlem33  42735  fourierdlem40  42742  fourierdlem41  42743  fourierdlem42  42744  fourierdlem43  42745  fourierdlem44  42746  fourierdlem46  42747  fourierdlem47  42748  fourierdlem48  42749  fourierdlem50  42751  fourierdlem63  42764  fourierdlem64  42765  fourierdlem65  42766  fourierdlem73  42774  fourierdlem74  42775  fourierdlem75  42776  fourierdlem76  42777  fourierdlem77  42778  fourierdlem78  42779  fourierdlem79  42780  fourierdlem87  42788  fourierdlem91  42792  fourierdlem92  42793  fourierdlem103  42804  fourierdlem104  42805  fouriersw  42826  etransclem19  42848  etransclem23  42852  etransclem48  42877  ioorrnopnlem  42899  iundjiun  43052  omeiunltfirp  43111  caratheodorylem1  43118  hoicvr  43140  hoidmv1lelem2  43184  hoidmvlelem2  43188  hoiqssbllem2  43215  vonioolem1  43272  vonicclem1  43275  smflimlem4  43360  smfmullem1  43376  iccpartgt  43897  perfectALTVlem2  44193  bgoldbtbndlem2  44277  pgrple2abl  44720  logbpw2m1  44934  dignn0ldlem  44969  2itscp  45148
  Copyright terms: Public domain W3C validator