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

Theorem 3eqtr2rd 2322
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1  |-  ( ph  ->  A  =  B )
3eqtr2d.2  |-  ( ph  ->  C  =  B )
3eqtr2d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtr2rd  |-  ( ph  ->  D  =  A )

Proof of Theorem 3eqtr2rd
StepHypRef Expression
1 3eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr2d.2 . . 3  |-  ( ph  ->  C  =  B )
31, 2eqtr4d 2318 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2316 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  nneob  6650  faclbnd2  11304  cats1un  11476  cjmulval  11630  fsumsplit  12212  fzosump1  12217  bcxmas  12294  trireciplem  12320  geo2sum  12329  geo2lim  12331  geoisum1c  12336  mertenslem1  12340  eftlub  12389  tanadd  12447  addsin  12450  subsin  12451  subcos  12455  sadadd2lem2  12641  qredeu  12786  zsqrelqelz  12829  4sqlem15  13006  resssetc  13924  resscatc  13937  curfcl  14006  conjghm  14713  gasubg  14756  dfod2  14877  efginvrel2  15036  efgcpbllemb  15064  odadd2  15141  frgpnabllem1  15161  pws1  15399  prdslmodd  15726  psrlmod  16146  znunithash  16518  restcld  16903  clmneg  18579  itg2monolem1  19105  itgconst  19173  dvexp  19302  dvfsumabs  19370  dvtaylp  19749  taylthlem2  19753  tangtx  19873  logsqr  20051  lawcoslem1  20113  chordthmlem2  20130  chordthmlem4  20132  tanatan  20215  atanbndlem  20221  amgmlem  20284  basellem3  20320  basellem5  20322  dvdsmulf1o  20434  chtub  20451  fsumvma  20452  lgsquad2lem1  20597  2sqlem8  20611  dchrmusum2  20643  logsqvma  20691  pntrlog2bndlem4  20729  gxsuc  20939  gxnn0add  20941  vc0  21125  hvsubdistr2  21629  adjlnop  22666  adjcoi  22680  cnvbraval  22690  xrge0pluscn  23322  cvmliftlem6  23821  cvmliftlem10  23825  cvmlift2lem3  23836  brbtwn2  24533  ax5seglem1  24556  axcontlem2  24593  axcontlem4  24595  bpolydiflem  24789  rltrran  25414  mslb1  25607  heibor  26545  ghomdiv  26574  frlmlbs  27249  proot1ex  27520  sigarperm  27850  sinhpcosh  28210  bnj553  28930  3atlem1  29672  atmod3i2  30054  trljat2  30356  cdleme1  30416  cdlemh2  31005  dihglblem3N  31485  dih1dimatlem0  31518  djhlsmcl  31604  mapdpglem30  31892  hdmapneg  32039  hgmapval1  32086  hgmapmul  32088
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator