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

Theorem 3eqtr2rd 2515
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 2511 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtr2d 2509 1  |-  ( ph  ->  D  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  nneob  7298  modeqmodmin  12020  faclbnd2  12333  cats1un  12660  cjmulval  12937  fsumsplit  13521  fzosump1  13526  bcxmas  13606  trireciplem  13632  geo2sum  13641  geo2lim  13643  geoisum1c  13648  mertenslem1  13652  eftlub  13701  tanadd  13759  addsin  13762  subsin  13763  subcos  13767  sadadd2lem2  13955  qredeu  14103  zsqrtelqelz  14146  4sqlem15  14332  resssetc  15273  resscatc  15286  curfcl  15355  conjghm  16092  gasubg  16135  dfod2  16382  efginvrel2  16541  efgcpbllemb  16569  odadd2  16648  frgpnabllem1  16668  srgbinomlem3  16981  pws1  17049  prdslmodd  17398  psrlmod  17825  znunithash  18370  frlmipval  18577  frlmlbs  18598  restcld  19439  clmneg  21316  rrxds  21560  itg2monolem1  21892  itgconst  21960  dvexp  22091  dvfsumabs  22159  dvtaylp  22499  taylthlem2  22503  tangtx  22631  logsqrt  22813  lawcoslem1  22875  chordthmlem2  22892  chordthmlem4  22894  tanatan  22978  atanbndlem  22984  amgmlem  23047  basellem3  23084  basellem5  23086  dvdsmulf1o  23198  chtub  23215  fsumvma  23216  lgsquad2lem1  23361  2sqlem8  23375  dchrmusum2  23407  logsqvma  23455  pntrlog2bndlem4  23493  miriso  23763  lmieu  23827  ttgcontlem1  23864  brbtwn2  23884  ax5seglem1  23907  axcontlem2  23944  axcontlem4  23946  gxcom  24947  gxsuc  24950  gxnn0add  24952  vc0  25138  hvsubdistr2  25643  adjlnop  26681  adjcoi  26695  cnvbraval  26705  fpwrelmap  27228  archirngz  27395  archiabllem1b  27398  xrge0pluscn  27558  esumfzf  27715  volmeas  27843  cvmliftlem6  28375  cvmliftlem10  28379  cvmlift2lem3  28390  fprodsplit  28672  risefallfac  28723  bpolydiflem  29393  sin2h  29622  heibor  29920  ghomdiv  29949  proot1ex  30766  fourierdlem92  31499  sigarperm  31544  sigaradd  31550  lincresunit3lem2  32154  sinhpcosh  32215  bnj553  33035  3atlem1  34279  atmod3i2  34661  trljat2  34963  cdleme1  35023  cdleme22eALTN  35141  cdlemh2  35612  dihglblem3N  36092  dih1dimatlem0  36125  djhlsmcl  36211  mapdpglem30  36499  hdmapneg  36646  hgmapval1  36693  hgmapmul  36695
  Copyright terms: Public domain W3C validator