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

Theorem lelttrd 10046
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 9979 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1317 . 2 (𝜑 → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 710 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976   class class class wbr 4577  cr 9791   < clt 9930  cle 9931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-pre-lttri 9866  ax-pre-lttrn 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936
This theorem is referenced by:  lt2msq1  10756  suprzcl  11289  ge0p1rp  11694  elfzolt3  12304  flflp1  12425  ltdifltdiv  12452  modsubdir  12556  seqf1olem1  12657  seqf1olem2  12658  expmulnbnd  12813  discr1  12817  faclbnd5  12902  bcp1nk  12921  hashfun  13036  swrds2  13479  abslt  13848  abs3lem  13872  fzomaxdiflem  13876  icodiamlt  13968  reccn2  14121  o1rlimmul  14143  caucvgrlem  14197  geomulcvg  14392  mertenslem1  14401  bpoly4  14575  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  sinltx  14704  eirrlem  14717  rpnnen2lem11  14738  ruclem10  14753  bitsfzolem  14940  bitsfzo  14941  bitsinv1lem  14947  smueqlem  14996  pcfaclem  15386  pockthg  15394  prmreclem5  15408  1arith  15415  4sqlem11  15443  4sqlem12  15444  4sqlem13  15445  coe1tmmul2  19413  ssblex  21984  nlmvscnlem2  22232  nlmvscnlem1  22233  nrginvrcnlem  22238  blcvx  22341  icccmplem2  22366  reconnlem2  22370  metdcnlem  22379  icopnfcnv  22480  nmoleub2lem3  22654  ipcnlem2  22769  ipcnlem1  22770  minveclem3b  22924  minveclem3  22925  pjthlem1  22933  pmltpclem2  22942  ivthlem2  22945  ovollb2lem  22980  iundisj  23040  uniioombllem3  23076  opnmbllem  23092  itg2monolem3  23242  itg2cnlem2  23252  dveflem  23463  dvferm2lem  23470  lhop1lem  23497  dvcnvre  23503  ftc1a  23521  ftc1lem4  23523  coeeulem  23701  dgradd2  23745  aaliou2b  23817  ulmdvlem1  23875  itgulm  23883  radcnvlem1  23888  radcnvlt1  23893  radcnvle  23895  psercnlem1  23900  pserdvlem1  23902  pserdv  23904  abelthlem2  23907  abelthlem7  23913  cosordlem  23998  tanord1  24004  efif1olem1  24009  logcnlem3  24107  logcnlem4  24108  efopnlem1  24119  logtayl  24123  cxpcn3lem  24205  birthdaylem3  24397  efrlim  24413  lgamgulmlem2  24473  lgamucov  24481  ftalem1  24516  ftalem2  24517  ftalem5  24520  basellem1  24524  basellem3  24526  perfectlem2  24672  bposlem1  24726  bposlem3  24728  bposlem6  24731  lgsdirprm  24773  lgsqrlem2  24789  lgseisen  24821  lgsquadlem1  24822  lgsquadlem2  24823  2sqlem8  24868  2sqblem  24873  dchrvmasumiflem1  24907  pntrmax  24970  pntlemc  25001  pntlemg  25004  pntlemr  25008  axpaschlem  25538  axlowdimlem16  25555  clwwisshclwwlem  26100  eupap1  26269  smcnlem  26737  minvecolem3  26922  pjhthlem1  27440  nmcexi  28075  iundisjf  28590  iundisjfi  28748  psgnfzto1stlem  28987  dya2icoseg  29472  subfaclim  30230  bcprod  30683  dnicn  31458  unbdqndv2lem1  31476  unbdqndv2lem2  31477  knoppndvlem18  31496  poimirlem6  32381  poimirlem7  32382  poimirlem12  32387  poimirlem15  32390  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem23  32398  poimirlem24  32399  opnmbllem0  32411  mblfinlem3  32414  mblfinlem4  32415  ftc1cnnclem  32449  ftc1anclem7  32457  isbnd3  32549  cntotbnd  32561  rrnequiv  32600  irrapxlem1  36200  pell14qrgapw  36254  monotoddzzfi  36321  ltrmynn0  36329  jm2.24nn  36340  acongeq  36364  jm2.26lem3  36382  jm3.1lem2  36399  binomcxplemnotnn0  37373  isosctrlem1ALT  37988  rfcnnnub  38014  zltlesub  38234  monoords  38248  supxrge  38292  infleinflem2  38325  fmul01lt1lem1  38448  fmul01lt1lem2  38449  lptre2pt  38504  addlimc  38512  0ellimcdiv  38513  limclner  38515  climleltrp  38540  icccncfext  38570  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnmul  38630  iblspltprt  38662  itgspltprt  38668  stoweidlem5  38695  stoweidlem11  38701  stoweidlem13  38703  stoweidlem14  38704  stoweidlem25  38715  stoweidlem26  38716  stoweidlem42  38732  stoweidlem59  38749  stoweid  38753  wallispilem3  38757  wallispilem4  38758  wallispilem5  38759  fourierdlem10  38807  fourierdlem11  38808  fourierdlem12  38809  fourierdlem15  38812  fourierdlem20  38817  fourierdlem24  38821  fourierdlem30  38827  fourierdlem31  38828  fourierdlem33  38830  fourierdlem40  38837  fourierdlem41  38838  fourierdlem42  38839  fourierdlem43  38840  fourierdlem44  38841  fourierdlem46  38842  fourierdlem47  38843  fourierdlem48  38844  fourierdlem50  38846  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem76  38872  fourierdlem77  38873  fourierdlem78  38874  fourierdlem79  38875  fourierdlem87  38883  fourierdlem91  38887  fourierdlem92  38888  fourierdlem103  38899  fourierdlem104  38900  fouriersw  38921  etransclem19  38943  etransclem23  38947  etransclem48  38972  ioorrnopnlem  38997  iundjiun  39150  omeiunltfirp  39206  caratheodorylem1  39213  hoicvr  39235  hoidmv1lelem2  39279  hoidmvlelem2  39283  hoiqssbllem2  39310  vonioolem1  39368  vonicclem1  39371  smflimlem4  39457  smfmullem1  39473  iccpartgt  39763  perfectALTVlem2  39963  bgoldbtbndlem2  40020  clwwisshclwwslem  41229  pgrple2abl  41935  logbpw2m1  42154  dignn0ldlem  42189
  Copyright terms: Public domain W3C validator