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

Theorem 3eqtrrd 2333
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 2328 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2329 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  iunfictbso  7757  axcnre  8802  fseq1p1m1  10873  seqf1olem1  11101  expmulz  11164  expubnd  11178  subsq  11226  bcm1k  11343  bcpasc  11349  crim  11616  rereb  11621  rlimrecl  12070  iseraltlem2  12171  fsumparts  12280  isumshft  12314  geoserg  12340  efsub  12396  sincossq  12472  efieq1re  12495  eucalg  12773  phiprmpw  12860  coprimeprodsq  12878  pythagtriplem15  12898  pythagtriplem17  12900  fldivp1  12961  1arithlem4  12989  setsid  13203  pwsbas  13402  invfuc  13864  latdisdlem  14308  odinv  14890  frgpuplem  15097  gexexlem  15160  gsumdixp  15408  mplcoe1  16225  ply1coe  16384  cnfldsub  16418  mretopd  16845  upxp  17333  uptx  17335  itgmulc2lem2  19203  r1pid  19561  coeeulem  19622  fta1lem  19703  aaliou3lem8  19741  eff1olem  19926  logcnlem4  20008  root1cj  20112  angpieqvdlem  20141  quad2  20151  dcubic  20158  quart1  20168  jensen  20299  ftalem5  20330  basellem8  20341  chpchtsum  20474  logfaclbnd  20477  perfectlem2  20485  2sqlem3  20621  dchrvmasum2lem  20661  dchrvmasumiflem2  20667  selberglem2  20711  selberg3r  20734  pntlem3  20774  ostth2  20802  ostth3  20803  nmbdoplbi  22620  nmcopexi  22623  nmbdfnlbi  22645  nmcfnexi  22647  nmcfnlbi  22648  hstoh  22828  ballotlemi1  23077  ballotlemii  23078  ballotlemic  23081  ballotlem1c  23082  lt2addrd  23264  xlt2addrd  23268  relexprel  24046  colinearalglem1  24606  axlowdimlem16  24657  axcontlem4  24667  itgmulc2nclem2  25018  areacirclem2  25028  areacirclem5  25032  cntotbnd  26623  rmydbl  27128  jm2.18  27184  jm2.19  27189  proot1hash  27622  sigarac  27945  cevathlem2  27961  atmod2i2  30673  trljat1  30977  trljat2  30978  cdleme9  31064  cdleme15b  31086  cdleme20c  31122  cdleme22eALTN  31156  dvhopN  31928  doca2N  31938  cdlemn10  32018  dochocss  32178  djhlj  32213  dihprrnlem1N  32236  dihprrnlem2  32237  lcfl7lem  32311  lclkrlem2c  32321  hgmapadd  32709  hdmapinvlem3  32735  hgmapvvlem1  32738
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator