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

Theorem 3eqtrrd 2403
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 2398 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2399 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647
This theorem is referenced by:  iunfictbso  7888  axcnre  8933  fseq1p1m1  11012  seqf1olem1  11249  expmulz  11313  expubnd  11327  subsq  11375  bcm1k  11493  bcpasc  11499  crim  11807  rereb  11812  rlimrecl  12261  iseraltlem2  12363  fsumparts  12472  isumshft  12506  geoserg  12532  efsub  12588  sincossq  12664  efieq1re  12687  eucalg  12965  phiprmpw  13052  coprimeprodsq  13070  pythagtriplem15  13090  pythagtriplem17  13092  fldivp1  13153  1arithlem4  13181  setsid  13395  pwsbas  13596  invfuc  14058  latdisdlem  14502  odinv  15084  frgpuplem  15291  gexexlem  15354  gsumdixp  15602  mplcoe1  16419  ply1coe  16578  cnfldsub  16619  mretopd  17046  upxp  17534  uptx  17536  itgmulc2lem2  19402  r1pid  19760  coeeulem  19821  fta1lem  19902  aaliou3lem8  19940  eff1olem  20128  logcnlem4  20214  root1cj  20318  angpieqvdlem  20347  quad2  20357  dcubic  20364  quart1  20374  jensen  20505  ftalem5  20537  basellem8  20548  chpchtsum  20681  logfaclbnd  20684  perfectlem2  20692  2sqlem3  20828  dchrvmasum2lem  20868  dchrvmasumiflem2  20874  selberglem2  20918  selberg3r  20941  pntlem3  20981  ostth2  21009  ostth3  21010  nmbdoplbi  22917  nmcopexi  22920  nmbdfnlbi  22942  nmcfnexi  22944  nmcfnlbi  22945  hstoh  23125  lt2addrd  23519  xlt2addrd  23524  qqhnm  23846  ballotlemi1  24208  ballotlemii  24209  ballotlemic  24212  ballotlem1c  24213  lgamgulmlem5  24265  lgamgulm2  24268  relexprel  24618  colinearalglem1  25276  axlowdimlem16  25327  axcontlem4  25337  itgmulc2nclem2  25690  areacirclem2  25700  areacirclem5  25704  cntotbnd  26026  rmydbl  26531  jm2.18  26587  jm2.19  26592  proot1hash  27025  sigarac  27348  cevathlem2  27364  atmod2i2  30122  trljat1  30426  trljat2  30427  cdleme9  30513  cdleme15b  30535  cdleme20c  30571  cdleme22eALTN  30605  dvhopN  31377  doca2N  31387  cdlemn10  31467  dochocss  31627  djhlj  31662  dihprrnlem1N  31685  dihprrnlem2  31686  lcfl7lem  31760  lclkrlem2c  31770  hgmapadd  32158  hdmapinvlem3  32184  hgmapvvlem1  32187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359
  Copyright terms: Public domain W3C validator