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

Theorem 3eqtrrd 2649
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 2644 . 2 (𝜑𝐴 = 𝐶)
4 3eqtrd.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2645 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  fimacnvinrn  6256  fvcofneq  6275  iunfictbso  8820  axcnre  9864  fseq1p1m1  12283  seqf1olem1  12702  expmulz  12768  expubnd  12783  subsq  12834  bcm1k  12964  bcpasc  12970  cshwcshid  13424  crim  13703  rereb  13708  rlimrecl  14159  iseraltlem2  14261  fsumparts  14379  isumshft  14410  geoserg  14437  efsub  14669  sincossq  14745  efieq1re  14768  eucalg  15138  lcmfunsnlem  15192  phiprmpw  15319  modprmn0modprm0  15350  coprimeprodsq  15351  pythagtriplem15  15372  pythagtriplem17  15374  fldivp1  15439  1arithlem4  15468  setsidvald  15721  setsid  15742  pwsbas  15970  invfuc  16457  latdisdlem  17012  odinv  17801  frgpuplem  18008  gexexlem  18078  srgbinomlem4  18366  gsumdixp  18432  mplcoe1  19286  evlsvarsrng  19349  ply1idvr1  19484  ply1coe  19487  evls1varsrng  19525  cnfldsub  19593  mat1scmat  20164  m1detdiag  20222  mdetunilem7  20243  madugsum  20268  pm2mpmhmlem2  20443  mretopd  20706  upxp  21236  uptx  21238  imasdsf1olem  21988  clmvs2  22702  cphipipcj  22808  cphipval2  22848  itgmulc2lem2  23405  r1pid  23723  coeeulem  23784  fta1lem  23866  aaliou3lem8  23904  eff1olem  24098  tanarg  24169  logcnlem4  24191  root1cj  24297  angpieqvdlem  24355  quad2  24366  dcubic  24373  quart1  24383  jensen  24515  lgamgulmlem5  24559  lgamgulm2  24562  ftalem5  24603  basellem8  24614  chpchtsum  24744  logfaclbnd  24747  perfectlem2  24755  gausslemma2dlem1a  24890  2sqlem3  24945  dchrvmasum2lem  24985  dchrvmasumiflem2  24991  selberglem2  25035  selberg3r  25058  pntlem3  25098  ostth2  25126  ostth3  25127  krippenlem  25385  colinearalglem1  25586  axlowdimlem16  25637  axcontlem4  25647  nmbdoplbi  28267  nmcopexi  28270  nmbdfnlbi  28292  nmcfnexi  28294  nmcfnlbi  28295  hstoh  28475  fcobij  28888  lt2addrd  28903  xlt2addrd  28913  isarchi3  29072  archirngz  29074  symgfcoeu  29176  submatminr1  29204  mdetpmtr1  29217  madjusmdetlem1  29221  qqhnm  29362  esumfzf  29458  ddemeas  29626  sseqp1  29784  ballotlemi1  29891  ballotlemii  29892  ballotlemic  29895  ballotlem1c  29896  elmrsubrn  30671  cos2h  32570  itg2addnclem  32631  itgmulc2nclem2  32647  areacirclem1  32670  areacirclem4  32673  cntotbnd  32765  atmod2i2  34166  trljat1  34471  trljat2  34472  cdleme9  34558  cdleme15b  34580  cdleme20c  34617  cdleme22eALTN  34651  dvhopN  35423  doca2N  35433  cdlemn10  35513  dochocss  35673  djhlj  35708  dihprrnlem1N  35731  dihprrnlem2  35732  lcfl7lem  35806  lclkrlem2c  35816  hgmapadd  36204  hdmapinvlem3  36230  hgmapvvlem1  36233  rmydbl  36523  jm2.18  36573  jm2.19  36578  proot1hash  36797  dssmapnvod  37334  binomcxplemnotnn0  37577  oddfl  38430  dstregt0  38434  supsubc  38510  fsumsplit1  38639  mccllem  38664  ellimcabssub0  38684  sumnnodd  38697  climresmpt  38726  coskpi2  38749  cosknegpi  38752  dvsinax  38801  dvnmptdivc  38828  dvnxpaek  38832  dvnmul  38833  dvmptfprodlem  38834  ditgeqiooicc  38852  itgioocnicc  38869  itgspltprt  38871  wallispi2lem2  38965  dirkerper  38989  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem18  39018  fourierdlem19  39019  fourierdlem33  39033  fourierdlem35  39035  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem53  39052  fourierdlem63  39062  fourierdlem65  39064  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem90  39089  fourierdlem93  39092  fourierdlem95  39094  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem111  39110  fourierswlem  39123  fouriersw  39124  etransclem4  39131  etransclem9  39136  etransclem28  39155  etransclem35  39162  etransclem38  39165  sge0tsms  39273  sge0sup  39284  sge0resplit  39299  sge0split  39302  sge0ss  39305  sge0rpcpnf  39314  sge0isum  39320  sge0xadd  39328  sge0seq  39339  ismeannd  39360  caratheodorylem1  39416  isomenndlem  39420  hoicvrrex  39446  ovn0lem  39455  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnlecvr2  39500  voncmpl  39511  hspmbllem1  39516  hspmbllem2  39517  ovolval4lem1  39539  incsmf  39629  smfpimltmpt  39633  smfpimltxrmpt  39645  decsmf  39653  smfpimgtmpt  39667  smfpimgtxrmpt  39670  smfmullem1  39676  sigarac  39690  cevathlem2  39706  fmtnorec3  39998  fmtnorec4  39999  pwdif  40039  oddflALTV  40113  perfectALTVlem2  40165  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  c0snmgmhm  41704  funcrngcsetc  41790  funcringcsetc  41827  ply1mulgsum  41972  lindslinindsimp2lem5  42045  m1modmmod  42110  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem2  42214
  Copyright terms: Public domain W3C validator