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

Theorem 3eqtrrd 2845
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtrd.1 (𝜑𝐴 = 𝐵)
3eqtrd.2 (𝜑𝐵 = 𝐶)
3eqtrd.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
3eqtrrd (𝜑𝐷 = 𝐴)

Proof of Theorem 3eqtrrd
StepHypRef Expression
1 3eqtrd.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2840 . 2 (𝜑𝐴 = 𝐶)
4 3eqtrd.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2841 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799
This theorem is referenced by:  fimacnvinrn  6570  fvcofneq  6589  iunfictbso  9220  axcnre  10270  fseq1p1m1  12637  seqf1olem1  13063  expmulz  13129  expubnd  13144  subsq  13195  bcm1k  13322  bcpasc  13328  cshwcshid  13797  crim  14078  rereb  14083  rlimrecl  14534  iseraltlem2  14636  fsumparts  14760  isumshft  14793  geoserg  14820  efsub  15050  sincossq  15126  efieq1re  15149  eucalg  15519  lcmfunsnlem  15573  phiprmpw  15698  modprmn0modprm0  15729  coprimeprodsq  15730  pythagtriplem15  15751  pythagtriplem17  15753  fldivp1  15818  1arithlem4  15847  setsidvald  16100  setsid  16125  pwsbas  16352  invfuc  16838  latdisdlem  17394  odinv  18179  frgpuplem  18386  gexexlem  18456  srgbinomlem4  18745  gsumdixp  18811  mplcoe1  19674  evlsvarsrng  19736  ply1idvr1  19871  ply1coe  19874  evls1varsrng  19912  cnfldsub  19982  mat1scmat  20556  m1detdiag  20614  mdetunilem7  20635  madugsum  20660  pm2mpmhmlem2  20837  mretopd  21110  upxp  21640  uptx  21642  imasdsf1olem  22391  clmvs2  23106  cphipipcj  23212  cphipval2  23252  itgmulc2lem2  23813  r1pid  24133  coeeulem  24194  fta1lem  24276  aaliou3lem8  24314  eff1olem  24509  tanarg  24579  logcnlem4  24605  root1cj  24711  angpieqvdlem  24769  quad2  24780  dcubic  24787  quart1  24797  jensen  24929  lgamgulmlem5  24973  lgamgulm2  24976  ftalem5  25017  basellem8  25028  chpchtsum  25158  logfaclbnd  25161  perfectlem2  25169  gausslemma2dlem1a  25304  2sqlem3  25359  dchrvmasum2lem  25399  dchrvmasumiflem2  25405  selberglem2  25449  selberg3r  25472  pntlem3  25512  ostth2  25540  ostth3  25541  krippenlem  25799  colinearalglem1  26000  axlowdimlem16  26051  axcontlem4  26061  clwlkclwwlkfo  27152  nmbdoplbi  29211  nmcopexi  29214  nmbdfnlbi  29236  nmcfnexi  29238  nmcfnlbi  29239  hstoh  29419  fcobij  29827  lt2addrd  29843  xlt2addrd  29850  isarchi3  30066  archirngz  30068  symgfcoeu  30170  submatminr1  30201  mdetpmtr1  30214  madjusmdetlem1  30218  qqhnm  30359  esumfzf  30456  ddemeas  30624  sseqp1  30782  ballotlemi1  30889  ballotlemii  30890  ballotlemic  30893  ballotlem1c  30894  fsum2dsub  31010  circlemeth  31043  hgt750lemb  31059  hgt750lema  31060  hgt750leme  31061  elmrsubrn  31740  cos2h  33713  itg2addnclem  33773  itgmulc2nclem2  33789  areacirclem1  33812  areacirclem4  33815  cntotbnd  33906  atmod2i2  35642  trljat1  35947  trljat2  35948  cdleme9  36034  cdleme15b  36056  cdleme20c  36092  cdleme22eALTN  36126  dvhopN  36897  doca2N  36907  cdlemn10  36987  dochocss  37147  djhlj  37182  dihprrnlem1N  37205  dihprrnlem2  37206  lcfl7lem  37280  lclkrlem2c  37290  hgmapadd  37675  hdmapinvlem3  37701  hgmapvvlem1  37704  rmydbl  38006  jm2.18  38056  jm2.19  38061  proot1hash  38279  dssmapnvod  38814  binomcxplemnotnn0  39055  oddfl  39971  dstregt0  39975  supsubc  40049  absimlere  40189  uzinico2  40269  fsumsplit1  40284  mccllem  40309  ellimcabssub0  40329  sumnnodd  40342  climresmpt  40371  limsupresuz  40415  liminfresuz  40496  coskpi2  40557  cosknegpi  40560  dvsinax  40607  dvnmptdivc  40633  dvnxpaek  40637  dvnmul  40638  dvmptfprodlem  40639  ditgeqiooicc  40655  itgioocnicc  40672  itgspltprt  40674  wallispi2lem2  40768  dirkerper  40792  dirkertrigeqlem2  40795  dirkertrigeqlem3  40796  dirkertrigeq  40797  dirkercncflem2  40800  dirkercncflem4  40802  fourierdlem18  40821  fourierdlem19  40822  fourierdlem33  40836  fourierdlem35  40838  fourierdlem41  40844  fourierdlem42  40845  fourierdlem48  40850  fourierdlem49  40851  fourierdlem50  40852  fourierdlem53  40855  fourierdlem63  40865  fourierdlem65  40867  fourierdlem73  40875  fourierdlem74  40876  fourierdlem75  40877  fourierdlem81  40883  fourierdlem82  40884  fourierdlem83  40885  fourierdlem84  40886  fourierdlem90  40892  fourierdlem93  40895  fourierdlem95  40897  fourierdlem103  40905  fourierdlem104  40906  fourierdlem107  40909  fourierdlem111  40913  fourierswlem  40926  fouriersw  40927  etransclem4  40934  etransclem9  40939  etransclem28  40958  etransclem35  40965  etransclem38  40968  sge0tsms  41076  sge0sup  41087  sge0resplit  41102  sge0split  41105  sge0ss  41108  sge0rpcpnf  41117  sge0isum  41123  sge0xadd  41131  sge0seq  41142  ismeannd  41163  caratheodorylem1  41222  isomenndlem  41226  hoicvrrex  41252  ovn0lem  41261  hoidmvlelem2  41292  hoidmvlelem3  41293  ovnlecvr2  41306  voncmpl  41317  hspmbllem1  41322  hspmbllem2  41323  ovolval4lem1  41345  incsmf  41433  smfpimltmpt  41437  smfpimltxrmpt  41449  decsmf  41457  smfpimgtmpt  41471  smfpimgtxrmpt  41474  smfmullem1  41480  smfsupmpt  41503  smfinfmpt  41507  smflimsuplem2  41509  sigarac  41523  cevathlem2  41539  fmtnorec3  42035  fmtnorec4  42036  pwdif  42076  oddflALTV  42150  perfectALTVlem2  42206  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  c0snmgmhm  42482  funcrngcsetc  42566  funcringcsetc  42603  ply1mulgsum  42746  lindslinindsimp2lem5  42819  m1modmmod  42884  nn0sumshdiglemA  42981  nn0sumshdiglemB  42982  nn0sumshdiglem2  42984
  Copyright terms: Public domain W3C validator