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

Theorem 3eqtr2rd 2443
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 2439 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.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:  nneob  6854  faclbnd2  11537  cats1un  11745  cjmulval  11905  fsumsplit  12488  fzosump1  12493  bcxmas  12570  trireciplem  12596  geo2sum  12605  geo2lim  12607  geoisum1c  12612  mertenslem1  12616  eftlub  12665  tanadd  12723  addsin  12726  subsin  12727  subcos  12731  sadadd2lem2  12917  qredeu  13062  zsqrelqelz  13105  4sqlem15  13282  resssetc  14202  resscatc  14215  curfcl  14284  conjghm  14991  gasubg  15034  dfod2  15155  efginvrel2  15314  efgcpbllemb  15342  odadd2  15419  frgpnabllem1  15439  pws1  15677  prdslmodd  16000  psrlmod  16420  znunithash  16800  restcld  17190  clmneg  19059  itg2monolem1  19595  itgconst  19663  dvexp  19792  dvfsumabs  19860  dvtaylp  20239  taylthlem2  20243  tangtx  20366  logsqr  20548  lawcoslem1  20610  chordthmlem2  20627  chordthmlem4  20629  tanatan  20712  atanbndlem  20718  amgmlem  20781  basellem3  20818  basellem5  20820  dvdsmulf1o  20932  chtub  20949  fsumvma  20950  lgsquad2lem1  21095  2sqlem8  21109  dchrmusum2  21141  logsqvma  21189  pntrlog2bndlem4  21227  gxcom  21810  gxsuc  21813  gxnn0add  21815  vc0  22001  hvsubdistr2  22505  adjlnop  23542  adjcoi  23556  cnvbraval  23566  xrge0adddir  24168  xrge0pluscn  24279  esumfzf  24412  volmeas  24540  cvmliftlem6  24930  cvmliftlem10  24934  cvmlift2lem3  24945  fprodsplit  25242  risefallfac  25292  brbtwn2  25748  ax5seglem1  25771  axcontlem2  25808  axcontlem4  25810  bpolydiflem  26004  heibor  26420  ghomdiv  26449  frlmlbs  27117  proot1ex  27388  sigarperm  27717  sigaradd  27723  sinhpcosh  28197  bnj553  28975  3atlem1  29965  atmod3i2  30347  trljat2  30649  cdleme1  30709  cdleme22eALTN  30827  cdlemh2  31298  dihglblem3N  31778  dih1dimatlem0  31811  djhlsmcl  31897  mapdpglem30  32185  hdmapneg  32332  hgmapval1  32379  hgmapmul  32381
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