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

Theorem lelttrd 10233
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 10166 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1366 . 2 (𝜑 → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 715 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030   class class class wbr 4685  cr 9973   < clt 10112  cle 10113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttri 10048  ax-pre-lttrn 10049
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118
This theorem is referenced by:  lt2msq1  10945  suprzcl  11495  ge0p1rp  11900  elfzolt3  12519  flflp1  12648  ltdifltdiv  12675  modsubdir  12779  seqf1olem1  12880  seqf1olem2  12881  expmulnbnd  13036  discr1  13040  faclbnd5  13125  bcp1nk  13144  hashfun  13262  swrds2  13731  abslt  14098  abs3lem  14122  fzomaxdiflem  14126  icodiamlt  14218  reccn2  14371  o1rlimmul  14393  caucvgrlem  14447  geomulcvg  14651  mertenslem1  14660  bpoly4  14834  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  sinltx  14963  eirrlem  14976  rpnnen2lem11  14997  ruclem10  15012  bitsfzolem  15203  bitsfzo  15204  bitsinv1lem  15210  smueqlem  15259  pcfaclem  15649  pockthg  15657  prmreclem5  15671  1arith  15678  4sqlem11  15706  4sqlem12  15707  4sqlem13  15708  coe1tmmul2  19694  ssblex  22280  nlmvscnlem2  22536  nlmvscnlem1  22537  nrginvrcnlem  22542  blcvx  22648  icccmplem2  22673  reconnlem2  22677  metdcnlem  22686  icopnfcnv  22788  nmoleub2lem3  22961  ipcnlem2  23089  ipcnlem1  23090  minveclem3b  23245  minveclem3  23246  pjthlem1  23254  pmltpclem2  23264  ivthlem2  23267  ovollb2lem  23302  iundisj  23362  uniioombllem3  23399  opnmbllem  23415  itg2monolem3  23564  itg2cnlem2  23574  dveflem  23787  dvferm2lem  23794  lhop1lem  23821  dvcnvre  23827  ftc1a  23845  ftc1lem4  23847  coeeulem  24025  dgradd2  24069  aaliou2b  24141  ulmdvlem1  24199  itgulm  24207  radcnvlem1  24212  radcnvlt1  24217  radcnvle  24219  psercnlem1  24224  pserdvlem1  24226  pserdv  24228  abelthlem2  24231  abelthlem7  24237  cosordlem  24322  tanord1  24328  efif1olem1  24333  logcnlem3  24435  logcnlem4  24436  efopnlem1  24447  logtayl  24451  cxpcn3lem  24533  birthdaylem3  24725  efrlim  24741  lgamgulmlem2  24801  lgamucov  24809  ftalem1  24844  ftalem2  24845  ftalem5  24848  basellem1  24852  basellem3  24854  perfectlem2  25000  bposlem1  25054  bposlem3  25056  bposlem6  25059  lgsdirprm  25101  lgsqrlem2  25117  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  2sqlem8  25196  2sqblem  25201  dchrvmasumiflem1  25235  pntrmax  25298  pntlemc  25329  pntlemg  25332  pntlemr  25336  axpaschlem  25865  axlowdimlem16  25882  clwwisshclwwslem  26971  smcnlem  27680  minvecolem3  27860  pjhthlem1  28378  nmcexi  29013  iundisjf  29528  iundisjfi  29683  psgnfzto1stlem  29978  dya2icoseg  30467  reprgt  30827  hgt750lem  30857  tgoldbachgtde  30866  subfaclim  31296  bcprod  31750  dnicn  32607  unbdqndv2lem1  32625  unbdqndv2lem2  32626  knoppndvlem18  32645  poimirlem6  33545  poimirlem7  33546  poimirlem12  33551  poimirlem15  33554  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem24  33563  opnmbllem0  33575  mblfinlem3  33578  mblfinlem4  33579  ftc1cnnclem  33613  ftc1anclem7  33621  isbnd3  33713  cntotbnd  33725  rrnequiv  33764  irrapxlem1  37703  pell14qrgapw  37757  monotoddzzfi  37824  ltrmynn0  37832  jm2.24nn  37843  acongeq  37867  jm2.26lem3  37885  jm3.1lem2  37902  binomcxplemnotnn0  38872  isosctrlem1ALT  39484  rfcnnnub  39509  zltlesub  39811  monoords  39825  supxrge  39867  infleinflem2  39900  uzubioo  40112  fmul01lt1lem1  40134  fmul01lt1lem2  40135  lptre2pt  40190  addlimc  40198  0ellimcdiv  40199  limclner  40201  climleltrp  40226  limsupubuzlem  40262  limsup10exlem  40322  icccncfext  40418  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  iblspltprt  40507  itgspltprt  40513  stoweidlem5  40540  stoweidlem11  40546  stoweidlem13  40548  stoweidlem14  40549  stoweidlem25  40560  stoweidlem26  40561  stoweidlem42  40577  stoweidlem59  40594  stoweid  40598  wallispilem3  40602  wallispilem4  40603  wallispilem5  40604  fourierdlem10  40652  fourierdlem11  40653  fourierdlem12  40654  fourierdlem15  40657  fourierdlem20  40662  fourierdlem24  40666  fourierdlem30  40672  fourierdlem31  40673  fourierdlem33  40675  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem43  40685  fourierdlem44  40686  fourierdlem46  40687  fourierdlem47  40688  fourierdlem48  40689  fourierdlem50  40691  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem77  40718  fourierdlem78  40719  fourierdlem79  40720  fourierdlem87  40728  fourierdlem91  40732  fourierdlem92  40733  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  etransclem19  40788  etransclem23  40792  etransclem48  40817  ioorrnopnlem  40842  iundjiun  40995  omeiunltfirp  41054  caratheodorylem1  41061  hoicvr  41083  hoidmv1lelem2  41127  hoidmvlelem2  41131  hoiqssbllem2  41158  vonioolem1  41215  vonicclem1  41218  smflimlem4  41303  smfmullem1  41319  iccpartgt  41688  perfectALTVlem2  41956  bgoldbtbndlem2  42019  pgrple2abl  42471  logbpw2m1  42686  dignn0ldlem  42721
  Copyright terms: Public domain W3C validator