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

Theorem 3eqtr2rd 2491
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 2487 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2485 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  nneob  7303  modeqmodmin  12038  faclbnd2  12351  cats1un  12683  cjmulval  12960  fsumsplit  13544  fzosump1  13549  bcxmas  13629  trireciplem  13655  geo2sum  13664  geo2lim  13666  geoisum1c  13671  mertenslem1  13675  fprodsplit  13752  eftlub  13826  tanadd  13884  addsin  13887  subsin  13888  subcos  13892  sadadd2lem2  14082  qredeu  14230  zsqrtelqelz  14273  4sqlem15  14459  resssetc  15398  resscatc  15411  curfcl  15480  conjghm  16276  gasubg  16319  dfod2  16565  efginvrel2  16724  efgcpbllemb  16752  odadd2  16834  frgpnabllem1  16856  srgbinomlem3  17172  pws1  17244  prdslmodd  17594  psrlmod  18033  znunithash  18581  frlmipval  18788  frlmlbs  18809  restcld  19651  clmneg  21559  rrxds  21803  itg2monolem1  22135  itgconst  22203  dvexp  22334  dvfsumabs  22402  dvtaylp  22743  taylthlem2  22747  tangtx  22876  logsqrt  23063  lawcoslem1  23125  chordthmlem2  23142  chordthmlem4  23144  tanatan  23228  atanbndlem  23234  amgmlem  23297  basellem3  23334  basellem5  23336  dvdsmulf1o  23448  chtub  23465  fsumvma  23466  lgsquad2lem1  23611  2sqlem8  23625  dchrmusum2  23657  logsqvma  23705  pntrlog2bndlem4  23743  miriso  24028  lmieu  24128  ttgcontlem1  24166  brbtwn2  24186  ax5seglem1  24209  axcontlem2  24246  axcontlem4  24248  gxcom  25249  gxsuc  25252  gxnn0add  25254  vc0  25440  hvsubdistr2  25945  adjlnop  26983  adjcoi  26997  cnvbraval  27007  fpwrelmap  27534  xrge0adddir  27660  archirngz  27711  archiabllem1b  27714  xrge0pluscn  27900  esumfzf  28053  volmeas  28181  cvmliftlem6  28713  cvmliftlem10  28717  cvmlift2lem3  28728  risefallfac  29122  bpolydiflem  29792  sin2h  30021  heibor  30293  ghomdiv  30322  proot1ex  31137  dirkerper  31832  fourierdlem83  31926  fourierdlem92  31935  sigarperm  32031  sigaradd  32037  estrreslem1  32609  lincresunit3lem2  32951  sinhpcosh  33004  bnj553  33824  3atlem1  35082  atmod3i2  35464  trljat2  35767  cdleme1  35827  cdleme22eALTN  35946  cdlemh2  36417  dihglblem3N  36897  dih1dimatlem0  36930  djhlsmcl  37016  mapdpglem30  37304  hdmapneg  37451  hgmapval1  37498  hgmapmul  37500
  Copyright terms: Public domain W3C validator