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

Theorem 3eqtrrd 2321
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 2316 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2317 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  iunfictbso  7737  axcnre  8782  fseq1p1m1  10853  seqf1olem1  11081  expmulz  11144  expubnd  11158  subsq  11206  bcm1k  11323  bcpasc  11329  crim  11596  rereb  11601  rlimrecl  12050  iseraltlem2  12151  fsumparts  12260  isumshft  12294  geoserg  12320  efsub  12376  sincossq  12452  efieq1re  12475  eucalg  12753  phiprmpw  12840  coprimeprodsq  12858  pythagtriplem15  12878  pythagtriplem17  12880  fldivp1  12941  1arithlem4  12969  setsid  13183  pwsbas  13382  invfuc  13844  latdisdlem  14288  odinv  14870  frgpuplem  15077  gexexlem  15140  gsumdixp  15388  mplcoe1  16205  ply1coe  16364  cnfldsub  16398  mretopd  16825  upxp  17313  uptx  17315  itgmulc2lem2  19183  r1pid  19541  coeeulem  19602  fta1lem  19683  aaliou3lem8  19721  eff1olem  19906  logcnlem4  19988  root1cj  20092  angpieqvdlem  20121  quad2  20131  dcubic  20138  quart1  20148  jensen  20279  ftalem5  20310  basellem8  20321  chpchtsum  20454  logfaclbnd  20457  perfectlem2  20465  2sqlem3  20601  dchrvmasum2lem  20641  dchrvmasumiflem2  20647  selberglem2  20691  selberg3r  20714  pntlem3  20754  ostth2  20782  ostth3  20783  nmbdoplbi  22600  nmcopexi  22603  nmbdfnlbi  22625  nmcfnexi  22627  nmcfnlbi  22628  hstoh  22808  ballotlemi1  23057  ballotlemii  23058  ballotlemic  23061  ballotlem1c  23062  relexprel  23438  colinearalglem1  23944  axlowdimlem16  23995  axcontlem4  24005  areacirclem2  24335  areacirclem5  24339  cntotbnd  25931  rmydbl  26436  jm2.18  26492  jm2.19  26497  proot1hash  26930  atmod2i2  29330  trljat1  29634  trljat2  29635  cdleme9  29721  cdleme15b  29743  cdleme20c  29779  cdleme22eALTN  29813  dvhopN  30585  doca2N  30595  cdlemn10  30675  dochocss  30835  djhlj  30870  dihprrnlem1N  30893  dihprrnlem2  30894  lcfl7lem  30968  lclkrlem2c  30978  hgmapadd  31366  hdmapinvlem3  31392  hgmapvvlem1  31395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-cleq 2277
  Copyright terms: Public domain W3C validator