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

Theorem 3eqtr2rd 2482
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 2478 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2476 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  nneob  7106  modeqmodmin  11783  faclbnd2  12082  cats1un  12385  cjmulval  12649  fsumsplit  13231  fzosump1  13236  bcxmas  13313  trireciplem  13339  geo2sum  13348  geo2lim  13350  geoisum1c  13355  mertenslem1  13359  eftlub  13408  tanadd  13466  addsin  13469  subsin  13470  subcos  13474  sadadd2lem2  13661  qredeu  13808  zsqrelqelz  13851  4sqlem15  14035  resssetc  14975  resscatc  14988  curfcl  15057  conjghm  15792  gasubg  15835  dfod2  16080  efginvrel2  16239  efgcpbllemb  16267  odadd2  16346  frgpnabllem1  16366  srgbinomlem3  16655  pws1  16723  prdslmodd  17065  psrlmod  17487  znunithash  18012  frlmipval  18219  frlmlbs  18240  restcld  18791  clmneg  20668  rrxds  20912  itg2monolem1  21243  itgconst  21311  dvexp  21442  dvfsumabs  21510  dvtaylp  21850  taylthlem2  21854  tangtx  21982  logsqr  22164  lawcoslem1  22226  chordthmlem2  22243  chordthmlem4  22245  tanatan  22329  atanbndlem  22335  amgmlem  22398  basellem3  22435  basellem5  22437  dvdsmulf1o  22549  chtub  22566  fsumvma  22567  lgsquad2lem1  22712  2sqlem8  22726  dchrmusum2  22758  logsqvma  22806  pntrlog2bndlem4  22844  miriso  23088  ttgcontlem1  23146  brbtwn2  23166  ax5seglem1  23189  axcontlem2  23226  axcontlem4  23228  gxcom  23771  gxsuc  23774  gxnn0add  23776  vc0  23962  hvsubdistr2  24467  adjlnop  25505  adjcoi  25519  cnvbraval  25529  fpwrelmap  26048  archirngz  26221  archiabllem1b  26224  xrge0pluscn  26385  esumfzf  26533  volmeas  26662  cvmliftlem6  27194  cvmliftlem10  27198  cvmlift2lem3  27209  fprodsplit  27491  risefallfac  27542  bpolydiflem  28212  sin2h  28441  heibor  28739  ghomdiv  28768  proot1ex  29588  sigarperm  29915  sigaradd  29921  lincresunit3lem2  31033  sinhpcosh  31094  bnj553  31910  3atlem1  33146  atmod3i2  33528  trljat2  33830  cdleme1  33890  cdleme22eALTN  34008  cdlemh2  34479  dihglblem3N  34959  dih1dimatlem0  34992  djhlsmcl  35078  mapdpglem30  35366  hdmapneg  35513  hgmapval1  35560  hgmapmul  35562
  Copyright terms: Public domain W3C validator