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

Theorem 3eqtrrd 2441
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 2436 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2437 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  iunfictbso  7951  axcnre  8995  fseq1p1m1  11077  seqf1olem1  11317  expmulz  11381  expubnd  11395  subsq  11443  bcm1k  11561  bcpasc  11567  crim  11875  rereb  11880  rlimrecl  12329  iseraltlem2  12431  fsumparts  12540  isumshft  12574  geoserg  12600  efsub  12656  sincossq  12732  efieq1re  12755  eucalg  13033  phiprmpw  13120  coprimeprodsq  13138  pythagtriplem15  13158  pythagtriplem17  13160  fldivp1  13221  1arithlem4  13249  setsid  13463  pwsbas  13664  invfuc  14126  latdisdlem  14570  odinv  15152  frgpuplem  15359  gexexlem  15422  gsumdixp  15670  mplcoe1  16483  ply1coe  16639  cnfldsub  16684  mretopd  17111  upxp  17608  uptx  17610  itgmulc2lem2  19677  r1pid  20035  coeeulem  20096  fta1lem  20177  aaliou3lem8  20215  eff1olem  20403  tanarg  20467  logcnlem4  20489  root1cj  20593  angpieqvdlem  20622  quad2  20632  dcubic  20639  quart1  20649  jensen  20780  ftalem5  20812  basellem8  20823  chpchtsum  20956  logfaclbnd  20959  perfectlem2  20967  2sqlem3  21103  dchrvmasum2lem  21143  dchrvmasumiflem2  21149  selberglem2  21193  selberg3r  21216  pntlem3  21256  ostth2  21284  ostth3  21285  nmbdoplbi  23480  nmcopexi  23483  nmbdfnlbi  23505  nmcfnexi  23507  nmcfnlbi  23508  hstoh  23688  fimacnvinrn  24000  lt2addrd  24068  xlt2addrd  24077  qqhnm  24327  esumfzf  24412  ballotlemi1  24713  ballotlemii  24714  ballotlemic  24717  ballotlem1c  24718  lgamgulmlem5  24770  lgamgulm2  24773  relexprel  25087  colinearalglem1  25749  axlowdimlem16  25800  axcontlem4  25810  itg2addnclem  26155  itgmulc2nclem2  26171  areacirclem2  26181  areacirclem5  26185  cntotbnd  26395  rmydbl  26893  jm2.18  26949  jm2.19  26954  proot1hash  27387  wallispi2lem2  27688  sigarac  27709  cevathlem2  27725  swrdccat3b  28031  usgra2adedglem1  28048  atmod2i2  30344  trljat1  30648  trljat2  30649  cdleme9  30735  cdleme15b  30757  cdleme20c  30793  cdleme22eALTN  30827  dvhopN  31599  doca2N  31609  cdlemn10  31689  dochocss  31849  djhlj  31884  dihprrnlem1N  31907  dihprrnlem2  31908  lcfl7lem  31982  lclkrlem2c  31992  hgmapadd  32380  hdmapinvlem3  32406  hgmapvvlem1  32409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator