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

Theorem 3eqtrrd 2322
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 2317 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2318 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625
This theorem is referenced by:  iunfictbso  7743  axcnre  8788  fseq1p1m1  10859  seqf1olem1  11087  expmulz  11150  expubnd  11164  subsq  11212  bcm1k  11329  bcpasc  11335  crim  11602  rereb  11607  rlimrecl  12056  iseraltlem2  12157  fsumparts  12266  isumshft  12300  geoserg  12326  efsub  12382  sincossq  12458  efieq1re  12481  eucalg  12759  phiprmpw  12846  coprimeprodsq  12864  pythagtriplem15  12884  pythagtriplem17  12886  fldivp1  12947  1arithlem4  12975  setsid  13189  pwsbas  13388  invfuc  13850  latdisdlem  14294  odinv  14876  frgpuplem  15083  gexexlem  15146  gsumdixp  15394  mplcoe1  16211  ply1coe  16370  cnfldsub  16404  mretopd  16831  upxp  17319  uptx  17321  itgmulc2lem2  19189  r1pid  19547  coeeulem  19608  fta1lem  19689  aaliou3lem8  19727  eff1olem  19912  logcnlem4  19994  root1cj  20098  angpieqvdlem  20127  quad2  20137  dcubic  20144  quart1  20154  jensen  20285  ftalem5  20316  basellem8  20327  chpchtsum  20460  logfaclbnd  20463  perfectlem2  20471  2sqlem3  20607  dchrvmasum2lem  20647  dchrvmasumiflem2  20653  selberglem2  20697  selberg3r  20720  pntlem3  20760  ostth2  20788  ostth3  20789  nmbdoplbi  22606  nmcopexi  22609  nmbdfnlbi  22631  nmcfnexi  22633  nmcfnlbi  22634  hstoh  22814  ballotlemi1  23063  ballotlemii  23064  ballotlemic  23067  ballotlem1c  23068  lt2addrd  23251  xlt2addrd  23255  relexprel  24033  colinearalglem1  24536  axlowdimlem16  24587  axcontlem4  24597  areacirclem2  24936  areacirclem5  24940  cntotbnd  26531  rmydbl  27036  jm2.18  27092  jm2.19  27097  proot1hash  27530  sigarac  27853  cevathlem2  27869  atmod2i2  30124  trljat1  30428  trljat2  30429  cdleme9  30515  cdleme15b  30537  cdleme20c  30573  cdleme22eALTN  30607  dvhopN  31379  doca2N  31389  cdlemn10  31469  dochocss  31629  djhlj  31664  dihprrnlem1N  31687  dihprrnlem2  31688  lcfl7lem  31762  lclkrlem2c  31772  hgmapadd  32160  hdmapinvlem3  32186  hgmapvvlem1  32189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-cleq 2278
  Copyright terms: Public domain W3C validator