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

Theorem 3eqtrrd 2475
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  |-  ( ph  ->  A  =  B )
3eqtrd.2  |-  ( ph  ->  B  =  C )
3eqtrd.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtrrd  |-  ( ph  ->  D  =  A )

Proof of Theorem 3eqtrrd
StepHypRef Expression
1 3eqtrd.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrd 2470 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2471 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  iunfictbso  7997  axcnre  9041  fseq1p1m1  11124  seqf1olem1  11364  expmulz  11428  expubnd  11442  subsq  11490  bcm1k  11608  bcpasc  11614  crim  11922  rereb  11927  rlimrecl  12376  iseraltlem2  12478  fsumparts  12587  isumshft  12621  geoserg  12647  efsub  12703  sincossq  12779  efieq1re  12802  eucalg  13080  phiprmpw  13167  coprimeprodsq  13185  pythagtriplem15  13205  pythagtriplem17  13207  fldivp1  13268  1arithlem4  13296  setsid  13510  pwsbas  13711  invfuc  14173  latdisdlem  14617  odinv  15199  frgpuplem  15406  gexexlem  15469  gsumdixp  15717  mplcoe1  16530  ply1coe  16686  cnfldsub  16731  mretopd  17158  upxp  17657  uptx  17659  itgmulc2lem2  19726  r1pid  20084  coeeulem  20145  fta1lem  20226  aaliou3lem8  20264  eff1olem  20452  tanarg  20516  logcnlem4  20538  root1cj  20642  angpieqvdlem  20671  quad2  20681  dcubic  20688  quart1  20698  jensen  20829  ftalem5  20861  basellem8  20872  chpchtsum  21005  logfaclbnd  21008  perfectlem2  21016  2sqlem3  21152  dchrvmasum2lem  21192  dchrvmasumiflem2  21198  selberglem2  21242  selberg3r  21265  pntlem3  21305  ostth2  21333  ostth3  21334  nmbdoplbi  23529  nmcopexi  23532  nmbdfnlbi  23554  nmcfnexi  23556  nmcfnlbi  23557  hstoh  23737  fimacnvinrn  24049  lt2addrd  24117  xlt2addrd  24126  qqhnm  24376  esumfzf  24461  ballotlemi1  24762  ballotlemii  24763  ballotlemic  24766  ballotlem1c  24767  lgamgulmlem5  24819  lgamgulm2  24822  relexprel  25136  colinearalglem1  25847  axlowdimlem16  25898  axcontlem4  25908  itg2addnclem  26258  itgmulc2nclem2  26274  areacirclem1  26294  areacirclem4  26297  cntotbnd  26507  rmydbl  27005  jm2.18  27061  jm2.19  27066  proot1hash  27498  wallispi2lem2  27799  sigarac  27820  cevathlem2  27836  usgra2adedglem1  28344  atmod2i2  30721  trljat1  31025  trljat2  31026  cdleme9  31112  cdleme15b  31134  cdleme20c  31170  cdleme22eALTN  31204  dvhopN  31976  doca2N  31986  cdlemn10  32066  dochocss  32226  djhlj  32261  dihprrnlem1N  32284  dihprrnlem2  32285  lcfl7lem  32359  lclkrlem2c  32369  hgmapadd  32757  hdmapinvlem3  32783  hgmapvvlem1  32786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator