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

Theorem lelttrd 11183
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 11115 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1371 . 2 (𝜑 → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 697 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2104   class class class wbr 5081  cr 10920   < clt 11059  cle 11060
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10978  ax-pre-lttri 10995  ax-pre-lttrn 10996
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3333  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11061  df-mnf 11062  df-xr 11063  df-ltxr 11064  df-le 11065
This theorem is referenced by:  lt2msq1  11909  suprzcl  12450  ge0p1rp  12811  elfzolt3  13447  flflp1  13577  ltdifltdiv  13604  modsubdir  13710  seqf1olem1  13812  seqf1olem2  13813  expmulnbnd  14000  discr1  14004  faclbnd5  14062  bcp1nk  14081  hashfun  14201  swrds2  14702  abslt  15075  abs3lem  15099  fzomaxdiflem  15103  icodiamlt  15196  reccn2  15355  o1rlimmul  15377  caucvgrlem  15433  geomulcvg  15637  mertenslem1  15645  bpoly4  15818  ef01bndlem  15942  sin01bnd  15943  cos01bnd  15944  sinltx  15947  eirrlem  15962  rpnnen2lem11  15982  ruclem10  15997  bitsfzolem  16190  bitsfzo  16191  bitsinv1lem  16197  smueqlem  16246  pcfaclem  16648  pockthg  16656  prmreclem5  16670  1arith  16677  4sqlem11  16705  4sqlem12  16706  4sqlem13  16707  coe1tmmul2  21496  ssblex  23630  nlmvscnlem2  23898  nlmvscnlem1  23899  nrginvrcnlem  23904  blcvx  24010  icccmplem2  24035  reconnlem2  24039  metdcnlem  24048  icopnfcnv  24154  nmoleub2lem3  24327  ipcnlem2  24457  ipcnlem1  24458  minveclem3b  24641  minveclem3  24642  pjthlem1  24650  pmltpclem2  24662  ivthlem2  24665  ovollb2lem  24701  iundisj  24761  uniioombllem3  24798  opnmbllem  24814  itg2monolem3  24966  itg2cnlem2  24976  dveflem  25192  dvferm2lem  25199  lhop1lem  25226  dvcnvre  25232  ftc1a  25250  ftc1lem4  25252  coeeulem  25434  dgradd2  25478  aaliou2b  25550  ulmdvlem1  25608  itgulm  25616  radcnvlem1  25621  radcnvlt1  25626  radcnvle  25628  psercnlem1  25633  pserdvlem1  25635  pserdv  25637  abelthlem2  25640  abelthlem7  25646  cosordlem  25735  tanord1  25742  efif1olem1  25747  logcnlem3  25848  logcnlem4  25849  efopnlem1  25860  logtayl  25864  cxpcn3lem  25949  birthdaylem3  26152  efrlim  26168  lgamgulmlem2  26228  lgamucov  26236  ftalem1  26271  ftalem2  26272  ftalem5  26275  basellem1  26279  basellem3  26281  perfectlem2  26427  bposlem1  26481  bposlem3  26483  bposlem6  26486  lgsdirprm  26528  lgsqrlem2  26544  lgseisen  26576  lgsquadlem1  26577  lgsquadlem2  26578  2sqlem8  26623  2sqblem  26628  dchrvmasumiflem1  26698  pntrmax  26761  pntlemc  26792  pntlemg  26795  pntlemr  26799  axpaschlem  27357  axlowdimlem16  27374  clwwisshclwwslem  28427  smcnlem  29108  minvecolem3  29287  pjhthlem1  29802  nmcexi  30437  iundisjf  30977  iundisjfi  31166  psgnfzto1stlem  31416  dya2icoseg  32293  reprgt  32650  hgt750lem  32680  tgoldbachgtde  32689  subfaclim  33199  bcprod  33753  dnicn  34721  unbdqndv2lem1  34738  unbdqndv2lem2  34739  knoppndvlem18  34758  poimirlem6  35831  poimirlem7  35832  poimirlem12  35837  poimirlem15  35840  poimirlem17  35842  poimirlem19  35844  poimirlem20  35845  poimirlem23  35848  poimirlem24  35849  opnmbllem0  35861  mblfinlem3  35864  mblfinlem4  35865  ftc1cnnclem  35896  ftc1anclem7  35904  isbnd3  35990  cntotbnd  36002  rrnequiv  36041  aks4d1p1p3  40277  aks4d1p1p2  40278  aks4d1p1p4  40279  aks4d1p1p7  40282  aks4d1p1p5  40283  aks4d1p5  40288  2np3bcnp1  40300  sticksstones10  40311  sticksstones12a  40313  sticksstones22  40324  metakunt1  40325  metakunt12  40336  metakunt28  40352  metakunt30  40354  flt4lem7  40691  fltnltalem  40694  fltnlta  40695  irrapxlem1  40839  pell14qrgapw  40893  monotoddzzfi  40960  ltrmynn0  40966  jm2.24nn  40977  acongeq  41001  jm2.26lem3  41019  jm3.1lem2  41036  binomcxplemnotnn0  42187  isosctrlem1ALT  42767  rfcnnnub  42792  zltlesub  43052  monoords  43064  supxrge  43105  infleinflem2  43138  uzubioo  43334  fmul01lt1lem1  43354  fmul01lt1lem2  43355  lptre2pt  43410  addlimc  43418  0ellimcdiv  43419  limclner  43421  climleltrp  43446  limsupubuzlem  43482  limsup10exlem  43542  icccncfext  43657  ioodvbdlimc1lem1  43701  ioodvbdlimc1lem2  43702  ioodvbdlimc2lem  43704  dvnmul  43713  iblspltprt  43743  itgspltprt  43749  stoweidlem5  43775  stoweidlem11  43781  stoweidlem13  43783  stoweidlem14  43784  stoweidlem25  43795  stoweidlem26  43796  stoweidlem42  43812  stoweidlem59  43829  stoweid  43833  wallispilem3  43837  wallispilem4  43838  wallispilem5  43839  fourierdlem10  43887  fourierdlem11  43888  fourierdlem12  43889  fourierdlem15  43892  fourierdlem20  43897  fourierdlem24  43901  fourierdlem30  43907  fourierdlem31  43908  fourierdlem33  43910  fourierdlem40  43917  fourierdlem41  43918  fourierdlem42  43919  fourierdlem43  43920  fourierdlem44  43921  fourierdlem46  43922  fourierdlem47  43923  fourierdlem48  43924  fourierdlem50  43926  fourierdlem63  43939  fourierdlem64  43940  fourierdlem65  43941  fourierdlem73  43949  fourierdlem74  43950  fourierdlem75  43951  fourierdlem76  43952  fourierdlem77  43953  fourierdlem78  43954  fourierdlem79  43955  fourierdlem87  43963  fourierdlem91  43967  fourierdlem92  43968  fourierdlem103  43979  fourierdlem104  43980  fouriersw  44001  etransclem19  44023  etransclem23  44027  etransclem48  44052  ioorrnopnlem  44074  iundjiun  44228  omeiunltfirp  44287  caratheodorylem1  44294  hoicvr  44316  hoidmv1lelem2  44360  hoidmvlelem2  44364  hoiqssbllem2  44391  vonioolem1  44448  vonicclem1  44451  smflimlem4  44542  smfmullem1  44559  iccpartgt  45123  perfectALTVlem2  45418  bgoldbtbndlem2  45502  pgrple2abl  45945  logbpw2m1  46157  dignn0ldlem  46192  2itscp  46371
  Copyright terms: Public domain W3C validator