Theorem 3eqtr4rd 2249

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	|- ( ph -> A = B )
3eqtr4d.2	|- ( ph -> C = A )
3eqtr4d.3	|- ( ph -> D = B )

Assertion

Ref	Expression
3eqtr4rd	|- ( ph -> D = C )

Proof of Theorem 3eqtr4rd

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

Syntax hints:   -> wi 4   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  csbcnvg  4863  fvco4  5653  phplem4  6954  phplem4on  6966  omp1eomlem  7198  ctssdclemn0  7214  recexnq  7505  prarloclemcalc  7617  addcomprg  7693  mulcomprg  7695  mulcmpblnrlemg  7855  axmulass  7988  divnegap  8781  modqlt  10480  modqmulnn  10489  seq3val  10607  seqvalcd  10608  seq3caopr3  10638  seqcaopr3g  10639  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seq3f1o  10664  bcval5  10910  omgadd  10949  seq3coll  10989  cjreb  11210  recj  11211  imcj  11219  imval2  11238  resqrexlemover  11354  sqrtmul  11379  amgm2  11462  maxabslemab  11550  xrmaxadd  11605  summodclem2a  11725  fsumf1o  11734  sumsnf  11753  sumsplitdc  11776  fsummulc2  11792  binom  11828  bcxmas  11833  expcnvap0  11846  expcnv  11848  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  prodmodclem3  11919  fprodseq  11927  fprodf1o  11932  prodsnf  11936  fprodfac  11959  fprodabs  11960  ege2le3  12015  efaddlem  12018  eftlub  12034  tanval3ap  12058  tannegap  12072  cosmul  12089  cos01bnd  12102  demoivreALT  12118  flodddiv4  12280  dfgcd3  12364  absmulgcd  12371  nninfctlemfo  12394  sqpweven  12530  2sqpwodd  12531  crth  12579  eulerthlema  12585  phisum  12596  pythagtriplem14  12633  pythagtriplem19  12638  pcmul  12657  pcfac  12706  4sqlem12  12758  ctiunctlemfo  12843  setsslnid  12917  qusgrp2  13482  mulgnngsum  13496  mulgnn0gsum  13497  mulgnn0p1  13502  mulgneg  13509  mulgnn0dir  13521  qusghm  13651  gsumfzconst  13710  gsumfzmhm  13712  srgpcomp  13785  opprrng  13872  opprring  13874  oppr1g  13877  invrfvald  13917  rdivmuldivd  13939  lmodvsmmulgdi  14118  lmodsubdi  14139  rmodislmodlem  14145  qusrhm  14323  quscrng  14328  mulgrhm  14404  txbasval  14772  plymullem1  15253  rplogbchbase  15455  sgmmul  15501  lgsdir2  15543  lgsdir  15545  lgsdi  15547  lgsdirnn0  15557  lgsdinn0  15558  lgsquad3  15594