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

Theorem 3eqtrrd 2778
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 2773 . 2 (𝜑𝐴 = 𝐶)
4 3eqtrd.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2774 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  fimacnvinrn  7026  fvcofneq  7047  iunfictbso  10058  axcnre  11108  fseq1p1m1  13524  seqf1olem1  13956  expmulz  14023  expubnd  14091  subsq  14123  bcm1k  14224  bcpasc  14230  cshwcshid  14725  crim  15009  rereb  15014  rlimrecl  15471  iseraltlem2  15576  fsumsplit1  15638  fsumparts  15699  isumshft  15732  geoserg  15759  pwdif  15761  efsub  15990  sincossq  16066  efieq1re  16089  eucalg  16471  lcmfunsnlem  16525  phiprmpw  16656  modprmn0modprm0  16687  coprimeprodsq  16688  pythagtriplem15  16709  pythagtriplem17  16711  fldivp1  16777  1arithlem4  16806  setsidvald  17079  setsidvaldOLD  17080  setsid  17088  pwsbas  17377  invfuc  17871  estrreslem1  18032  latdisdlem  18393  odinv  19351  frgpuplem  19562  gexexlem  19638  fincygsubgodd  19899  srgbinomlem4  19968  gsumdixp  20041  cnfldsub  20848  mplcoe1  21461  evlsvarsrng  21532  ply1idvr1  21687  ply1coe  21690  evls1varsrng  21729  mat1scmat  21911  m1detdiag  21969  mdetunilem7  21990  madugsum  22015  pm2mpmhmlem2  22191  mretopd  22466  upxp  22997  uptx  22999  imasdsf1olem  23749  clmvs2  24480  cphipipcj  24587  cphipval2  24628  itgmulc2lem2  25220  r1pid  25547  coeeulem  25608  fta1lem  25690  aaliou3lem8  25728  eff1olem  25927  tanarg  25997  logcnlem4  26023  root1cj  26132  angpieqvdlem  26201  quad2  26212  dcubic  26219  quart1  26229  jensen  26361  lgamgulmlem5  26405  lgamgulm2  26408  ftalem5  26449  basellem8  26460  chpchtsum  26590  logfaclbnd  26593  perfectlem2  26601  gausslemma2dlem1a  26736  2sqlem3  26791  dchrvmasum2lem  26867  dchrvmasumiflem2  26873  selberglem2  26917  selberg3r  26940  pntlem3  26980  ostth2  27008  ostth3  27009  madeoldsuc  27243  krippenlem  27681  colinearalglem1  27904  axlowdimlem16  27955  axcontlem4  27965  clwlkclwwlkfo  29002  nmbdoplbi  31015  nmcopexi  31018  nmbdfnlbi  31040  nmcfnexi  31042  nmcfnlbi  31043  hstoh  31223  fcobij  31693  lt2addrd  31710  xlt2addrd  31717  cshwrnid  31871  symgfcoeu  31989  cycpmconjslem2  32060  cycpmconjs  32061  isarchi3  32079  archirngz  32081  ghmquskerco  32251  dimkerim  32386  submatminr1  32455  mdetpmtr1  32468  madjusmdetlem1  32472  zarcmplem  32526  qqhnm  32635  esumfzf  32732  ddemeas  32899  sseqp1  33059  ballotlemi1  33166  ballotlemii  33167  ballotlemic  33170  ballotlem1c  33171  fsum2dsub  33284  circlemeth  33317  hgt750lemb  33333  hgt750lema  33334  hgt750leme  33335  elmrsubrn  34178  cos2h  36119  itg2addnclem  36179  itgmulc2nclem2  36195  areacirclem1  36216  areacirclem4  36219  cntotbnd  36305  atmod2i2  38375  trljat1  38679  trljat2  38680  cdleme9  38766  cdleme15b  38788  cdleme20c  38824  cdleme22eALTN  38858  dvhopN  39629  doca2N  39639  cdlemn10  39719  dochocss  39879  djhlj  39914  dihprrnlem1N  39937  dihprrnlem2  39938  lcfl7lem  40012  lclkrlem2c  40022  hgmapadd  40407  hdmapinvlem3  40433  hgmapvvlem1  40436  nn0expgcd  40868  zaddcomlem  40967  rmydbl  41311  jm2.18  41359  jm2.19  41364  proot1hash  41574  dssmapnvod  42384  binomcxplemnotnn0  42728  oddfl  43602  dstregt0  43606  supsubc  43678  absimlere  43805  uzinico2  43890  mccllem  43928  ellimcabssub0  43948  sumnnodd  43961  climresmpt  43990  limsupresuz  44034  liminfresuz  44115  coskpi2  44197  cosknegpi  44200  dvsinax  44244  dvnmptdivc  44269  dvnxpaek  44273  dvnmul  44274  dvmptfprodlem  44275  ditgeqiooicc  44291  itgioocnicc  44308  itgspltprt  44310  wallispi2lem2  44403  dirkerper  44427  dirkertrigeqlem2  44430  dirkertrigeqlem3  44431  dirkertrigeq  44432  dirkercncflem2  44435  dirkercncflem4  44437  fourierdlem18  44456  fourierdlem19  44457  fourierdlem33  44471  fourierdlem35  44473  fourierdlem41  44479  fourierdlem42  44480  fourierdlem48  44485  fourierdlem49  44486  fourierdlem50  44487  fourierdlem53  44490  fourierdlem63  44500  fourierdlem65  44502  fourierdlem73  44510  fourierdlem74  44511  fourierdlem75  44512  fourierdlem81  44518  fourierdlem82  44519  fourierdlem83  44520  fourierdlem84  44521  fourierdlem90  44527  fourierdlem93  44530  fourierdlem95  44532  fourierdlem103  44540  fourierdlem104  44541  fourierdlem107  44544  fourierdlem111  44548  fourierswlem  44561  fouriersw  44562  etransclem4  44569  etransclem9  44574  etransclem28  44593  etransclem35  44600  etransclem38  44603  sge0tsms  44711  sge0sup  44722  sge0resplit  44737  sge0split  44740  sge0ss  44743  sge0rpcpnf  44752  sge0isum  44758  sge0xadd  44766  sge0seq  44777  ismeannd  44798  caratheodorylem1  44857  isomenndlem  44861  hoicvrrex  44887  ovn0lem  44896  hoidmvlelem2  44927  hoidmvlelem3  44928  ovnlecvr2  44941  voncmpl  44952  hspmbllem1  44957  hspmbllem2  44958  ovolval4lem1  44980  incsmf  45073  smfpimltmpt  45077  smfpimltxrmptf  45089  decsmf  45098  smfpimgtmpt  45112  smfpimgtxrmptf  45115  smfmullem1  45122  smfinfmpt  45150  smflimsuplem2  45152  sigarac  45183  cevathlem2  45199  fmtnorec3  45830  fmtnorec4  45831  oddflALTV  45945  perfectALTVlem2  46004  nnsum4primeseven  46082  nnsum4primesevenALTV  46083  c0snmgmhm  46302  funcrngcsetc  46386  funcringcsetc  46423  ply1mulgsum  46561  lindslinindsimp2lem5  46633  m1modmmod  46697  nn0sumshdiglemA  46795  nn0sumshdiglemB  46796  nn0sumshdiglem2  46798  itschlc0yqe  46936
  Copyright terms: Public domain W3C validator