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

Theorem 3eqtrrd 2472
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 2467 . 2  |-  ( ph  ->  A  =  C )
4 3eqtrd.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2468 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  iunfictbso  7984  axcnre  9028  fseq1p1m1  11110  seqf1olem1  11350  expmulz  11414  expubnd  11428  subsq  11476  bcm1k  11594  bcpasc  11600  crim  11908  rereb  11913  rlimrecl  12362  iseraltlem2  12464  fsumparts  12573  isumshft  12607  geoserg  12633  efsub  12689  sincossq  12765  efieq1re  12788  eucalg  13066  phiprmpw  13153  coprimeprodsq  13171  pythagtriplem15  13191  pythagtriplem17  13193  fldivp1  13254  1arithlem4  13282  setsid  13496  pwsbas  13697  invfuc  14159  latdisdlem  14603  odinv  15185  frgpuplem  15392  gexexlem  15455  gsumdixp  15703  mplcoe1  16516  ply1coe  16672  cnfldsub  16717  mretopd  17144  upxp  17643  uptx  17645  itgmulc2lem2  19712  r1pid  20070  coeeulem  20131  fta1lem  20212  aaliou3lem8  20250  eff1olem  20438  tanarg  20502  logcnlem4  20524  root1cj  20628  angpieqvdlem  20657  quad2  20667  dcubic  20674  quart1  20684  jensen  20815  ftalem5  20847  basellem8  20858  chpchtsum  20991  logfaclbnd  20994  perfectlem2  21002  2sqlem3  21138  dchrvmasum2lem  21178  dchrvmasumiflem2  21184  selberglem2  21228  selberg3r  21251  pntlem3  21291  ostth2  21319  ostth3  21320  nmbdoplbi  23515  nmcopexi  23518  nmbdfnlbi  23540  nmcfnexi  23542  nmcfnlbi  23543  hstoh  23723  fimacnvinrn  24035  lt2addrd  24103  xlt2addrd  24112  qqhnm  24362  esumfzf  24447  ballotlemi1  24748  ballotlemii  24749  ballotlemic  24752  ballotlem1c  24753  lgamgulmlem5  24805  lgamgulm2  24808  relexprel  25122  colinearalglem1  25793  axlowdimlem16  25844  axcontlem4  25854  itg2addnclem  26202  itgmulc2nclem2  26218  areacirclem2  26228  areacirclem5  26232  cntotbnd  26442  rmydbl  26940  jm2.18  26996  jm2.19  27001  proot1hash  27434  wallispi2lem2  27735  sigarac  27756  cevathlem2  27772  swrdccat3b  28106  usgra2adedglem1  28192  atmod2i2  30498  trljat1  30802  trljat2  30803  cdleme9  30889  cdleme15b  30911  cdleme20c  30947  cdleme22eALTN  30981  dvhopN  31753  doca2N  31763  cdlemn10  31843  dochocss  32003  djhlj  32038  dihprrnlem1N  32061  dihprrnlem2  32062  lcfl7lem  32136  lclkrlem2c  32146  hgmapadd  32534  hdmapinvlem3  32560  hgmapvvlem1  32563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator