Theorem 3eqtr2rd 2663

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

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 |- ( ph -> A = B )
2		3eqtr2d.2	. . 3 |- ( ph -> C = B )
3	1, 2	eqtr4d 2659	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2657	1 |- ( ph -> D = A )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  nneob  7732  xp1d2m1eqxm1d2  11286  negmod  12715  modeqmodmin  12740  faclbnd2  13078  cats1un  13475  cjmulval  13885  fsumsplit  14471  fzosump1  14481  bcxmas  14567  trireciplem  14594  geo2sum  14604  geo2lim  14606  geoisum1c  14611  mertenslem1  14616  fprodsplit  14696  risefallfac  14755  bpolydiflem  14785  eftlub  14839  tanadd  14897  addsin  14900  subsin  14901  subcos  14905  sadadd2lem2  15172  qredeu  15372  zsqrtelqelz  15466  4sqlem15  15663  rcaninv  16454  resssetc  16742  resscatc  16755  estrreslem1  16777  curfcl  16872  mulgaddcomlem  17563  conjghm  17691  gasubg  17735  dfod2  17981  efginvrel2  18140  efgcpbllemb  18168  odadd2  18252  frgpnabllem1  18276  srgbinomlem3  18542  pws1  18616  prdslmodd  18969  psrlmod  19401  znunithash  19913  frlmipval  20118  frlmlbs  20136  restcld  20976  clmneg  22881  rrxds  23181  itg2monolem1  23517  itgconst  23585  dvexp  23716  dvfsumabs  23786  dvtaylp  24124  taylthlem2  24128  tangtx  24257  logsqrt  24450  lawcoslem1  24545  chordthmlem2  24560  chordthmlem4  24562  tanatan  24646  atanbndlem  24652  amgmlem  24716  basellem3  24809  basellem5  24811  dvdsmulf1o  24920  chtub  24937  fsumvma  24938  lgsquad2lem1  25109  2sqlem8  25151  dchrmusum2  25183  logsqvma  25231  pntrlog2bndlem4  25269  miriso  25565  lmieu  25676  sacgr  25722  ttgcontlem1  25765  brbtwn2  25785  ax5seglem1  25808  axcontlem2  25845  axcontlem4  25847  vc0  27429  hvsubdistr2  27907  adjlnop  28945  adjcoi  28959  cnvbraval  28969  fpwrelmap  29508  fsumiunle  29575  xrge0adddir  29692  archirngz  29743  archiabllem1b  29746  xrge0pluscn  29986  esumfzf  30131  esumiun  30156  volmeas  30294  omssubadd  30362  breprexplemc  30710  bnj553  30968  cvmliftlem6  31272  cvmliftlem10  31276  cvmlift2lem3  31287  finxpreclem4  33231  sin2h  33399  matunitlindflem2  33406  poimirlem16  33425  heibor  33620  ghomdiv  33691  3atlem1  34769  atmod3i2  35151  trljat2  35454  cdleme1  35514  cdleme22eALTN  35633  cdlemh2  36104  dihglblem3N  36584  dih1dimatlem0  36617  djhlsmcl  36703  mapdpglem30  36991  hdmapneg  37138  hgmapval1  37185  hgmapmul  37187  proot1ex  37779  dirkerper  40313  fourierdlem83  40406  fourierdlem92  40415  sigarperm  41049  sigaradd  41055  fmtnorec1  41449  lincresunit3lem2  42269  sinhpcosh  42481  amgmwlem  42548