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

Theorem 3eqtr2rd 2480
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 2476 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2474 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434
This theorem is referenced by:  nneob  7087  modeqmodmin  11764  faclbnd2  12063  cats1un  12366  cjmulval  12630  fsumsplit  13212  fzosump1  13217  bcxmas  13294  trireciplem  13320  geo2sum  13329  geo2lim  13331  geoisum1c  13336  mertenslem1  13340  eftlub  13389  tanadd  13447  addsin  13450  subsin  13451  subcos  13455  sadadd2lem2  13642  qredeu  13789  zsqrelqelz  13832  4sqlem15  14016  resssetc  14956  resscatc  14969  curfcl  15038  conjghm  15770  gasubg  15813  dfod2  16058  efginvrel2  16217  efgcpbllemb  16245  odadd2  16324  frgpnabllem1  16344  srgbinomlem3  16630  pws1  16698  prdslmodd  17028  psrlmod  17450  znunithash  17956  frlmipval  18163  frlmlbs  18184  restcld  18735  clmneg  20612  rrxds  20856  itg2monolem1  21187  itgconst  21255  dvexp  21386  dvfsumabs  21454  dvtaylp  21794  taylthlem2  21798  tangtx  21926  logsqr  22108  lawcoslem1  22170  chordthmlem2  22187  chordthmlem4  22189  tanatan  22273  atanbndlem  22279  amgmlem  22342  basellem3  22379  basellem5  22381  dvdsmulf1o  22493  chtub  22510  fsumvma  22511  lgsquad2lem1  22656  2sqlem8  22670  dchrmusum2  22702  logsqvma  22750  pntrlog2bndlem4  22788  miriso  23023  ttgcontlem1  23066  brbtwn2  23086  ax5seglem1  23109  axcontlem2  23146  axcontlem4  23148  gxcom  23691  gxsuc  23694  gxnn0add  23696  vc0  23882  hvsubdistr2  24387  adjlnop  25425  adjcoi  25439  cnvbraval  25449  fpwrelmap  25968  archirngz  26139  archiabllem1b  26142  xrge0pluscn  26306  esumfzf  26454  volmeas  26583  cvmliftlem6  27109  cvmliftlem10  27113  cvmlift2lem3  27124  fprodsplit  27405  risefallfac  27456  bpolydiflem  28126  sin2h  28347  heibor  28645  ghomdiv  28674  proot1ex  29494  sigarperm  29821  sigaradd  29827  lincresunit3lem2  30855  sinhpcosh  30916  bnj553  31725  3atlem1  32849  atmod3i2  33231  trljat2  33533  cdleme1  33593  cdleme22eALTN  33711  cdlemh2  34182  dihglblem3N  34662  dih1dimatlem0  34695  djhlsmcl  34781  mapdpglem30  35069  hdmapneg  35216  hgmapval1  35263  hgmapmul  35265
  Copyright terms: Public domain W3C validator