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

Theorem 3eqtrrd 2320
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 2315 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2316 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  iunfictbso  7741  axcnre  8786  fseq1p1m1  10857  seqf1olem1  11085  expmulz  11148  expubnd  11162  subsq  11210  bcm1k  11327  bcpasc  11333  crim  11600  rereb  11605  rlimrecl  12054  iseraltlem2  12155  fsumparts  12264  isumshft  12298  geoserg  12324  efsub  12380  sincossq  12456  efieq1re  12479  eucalg  12757  phiprmpw  12844  coprimeprodsq  12862  pythagtriplem15  12882  pythagtriplem17  12884  fldivp1  12945  1arithlem4  12973  setsid  13187  pwsbas  13386  invfuc  13848  latdisdlem  14292  odinv  14874  frgpuplem  15081  gexexlem  15144  gsumdixp  15392  mplcoe1  16209  ply1coe  16368  cnfldsub  16402  mretopd  16829  upxp  17317  uptx  17319  itgmulc2lem2  19187  r1pid  19545  coeeulem  19606  fta1lem  19687  aaliou3lem8  19725  eff1olem  19910  logcnlem4  19992  root1cj  20096  angpieqvdlem  20125  quad2  20135  dcubic  20142  quart1  20152  jensen  20283  ftalem5  20314  basellem8  20325  chpchtsum  20458  logfaclbnd  20461  perfectlem2  20469  2sqlem3  20605  dchrvmasum2lem  20645  dchrvmasumiflem2  20651  selberglem2  20695  selberg3r  20718  pntlem3  20758  ostth2  20786  ostth3  20787  nmbdoplbi  22604  nmcopexi  22607  nmbdfnlbi  22629  nmcfnexi  22631  nmcfnlbi  22632  hstoh  22812  ballotlemi1  23061  ballotlemii  23062  ballotlemic  23065  ballotlem1c  23066  lt2addrd  23249  xlt2addrd  23253  relexprel  24031  colinearalglem1  24534  axlowdimlem16  24585  axcontlem4  24595  areacirclem2  24925  areacirclem5  24929  cntotbnd  26520  rmydbl  27025  jm2.18  27081  jm2.19  27086  proot1hash  27519  sigarac  27842  cevathlem2  27858  atmod2i2  30051  trljat1  30355  trljat2  30356  cdleme9  30442  cdleme15b  30464  cdleme20c  30500  cdleme22eALTN  30534  dvhopN  31306  doca2N  31316  cdlemn10  31396  dochocss  31556  djhlj  31591  dihprrnlem1N  31614  dihprrnlem2  31615  lcfl7lem  31689  lclkrlem2c  31699  hgmapadd  32087  hdmapinvlem3  32113  hgmapvvlem1  32116
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 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator