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

Theorem 3eqtr2rd 2475
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 2471 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2469 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  nneob  6895  faclbnd2  11582  cats1un  11790  cjmulval  11950  fsumsplit  12533  fzosump1  12538  bcxmas  12615  trireciplem  12641  geo2sum  12650  geo2lim  12652  geoisum1c  12657  mertenslem1  12661  eftlub  12710  tanadd  12768  addsin  12771  subsin  12772  subcos  12776  sadadd2lem2  12962  qredeu  13107  zsqrelqelz  13150  4sqlem15  13327  resssetc  14247  resscatc  14260  curfcl  14329  conjghm  15036  gasubg  15079  dfod2  15200  efginvrel2  15359  efgcpbllemb  15387  odadd2  15464  frgpnabllem1  15484  pws1  15722  prdslmodd  16045  psrlmod  16465  znunithash  16845  restcld  17236  clmneg  19106  itg2monolem1  19642  itgconst  19710  dvexp  19839  dvfsumabs  19907  dvtaylp  20286  taylthlem2  20290  tangtx  20413  logsqr  20595  lawcoslem1  20657  chordthmlem2  20674  chordthmlem4  20676  tanatan  20759  atanbndlem  20765  amgmlem  20828  basellem3  20865  basellem5  20867  dvdsmulf1o  20979  chtub  20996  fsumvma  20997  lgsquad2lem1  21142  2sqlem8  21156  dchrmusum2  21188  logsqvma  21236  pntrlog2bndlem4  21274  gxcom  21857  gxsuc  21860  gxnn0add  21862  vc0  22048  hvsubdistr2  22552  adjlnop  23589  adjcoi  23603  cnvbraval  23613  xrge0adddir  24215  xrge0pluscn  24326  esumfzf  24459  volmeas  24587  cvmliftlem6  24977  cvmliftlem10  24981  cvmlift2lem3  24992  fprodsplit  25289  risefallfac  25340  brbtwn2  25844  ax5seglem1  25867  axcontlem2  25904  axcontlem4  25906  bpolydiflem  26100  heibor  26530  ghomdiv  26559  frlmlbs  27226  proot1ex  27497  sigarperm  27826  sigaradd  27832  sinhpcosh  28483  bnj553  29269  3atlem1  30280  atmod3i2  30662  trljat2  30964  cdleme1  31024  cdleme22eALTN  31142  cdlemh2  31613  dihglblem3N  32093  dih1dimatlem0  32126  djhlsmcl  32212  mapdpglem30  32500  hdmapneg  32647  hgmapval1  32694  hgmapmul  32696
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 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator