Theorem 3eqtr4rd 2240

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 2232	. 2 |- ( ph -> D = A )
4		3eqtr4d.2	. 2 |- ( ph -> C = A )
5	3, 4	eqtr4d 2232	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbcnvg  4850  fvco4  5633  phplem4  6916  phplem4on  6928  omp1eomlem  7160  ctssdclemn0  7176  recexnq  7457  prarloclemcalc  7569  addcomprg  7645  mulcomprg  7647  mulcmpblnrlemg  7807  axmulass  7940  divnegap  8733  modqlt  10425  modqmulnn  10434  seq3val  10552  seqvalcd  10553  seq3caopr3  10583  seqcaopr3g  10584  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1o  10609  bcval5  10855  omgadd  10894  seq3coll  10934  cjreb  11031  recj  11032  imcj  11040  imval2  11059  resqrexlemover  11175  sqrtmul  11200  amgm2  11283  maxabslemab  11371  xrmaxadd  11426  summodclem2a  11546  fsumf1o  11555  sumsnf  11574  sumsplitdc  11597  fsummulc2  11613  binom  11649  bcxmas  11654  expcnvap0  11667  expcnv  11669  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  prodmodclem3  11740  fprodseq  11748  fprodf1o  11753  prodsnf  11757  fprodfac  11780  fprodabs  11781  ege2le3  11836  efaddlem  11839  eftlub  11855  tanval3ap  11879  tannegap  11893  cosmul  11910  cos01bnd  11923  demoivreALT  11939  flodddiv4  12101  dfgcd3  12177  absmulgcd  12184  nninfctlemfo  12207  sqpweven  12343  2sqpwodd  12344  crth  12392  eulerthlema  12398  phisum  12409  pythagtriplem14  12446  pythagtriplem19  12451  pcmul  12470  pcfac  12519  4sqlem12  12571  ctiunctlemfo  12656  setsslnid  12730  qusgrp2  13243  mulgnngsum  13257  mulgnn0gsum  13258  mulgnn0p1  13263  mulgneg  13270  mulgnn0dir  13282  qusghm  13412  gsumfzconst  13471  gsumfzmhm  13473  srgpcomp  13546  opprrng  13633  opprring  13635  oppr1g  13638  invrfvald  13678  rdivmuldivd  13700  lmodvsmmulgdi  13879  lmodsubdi  13900  rmodislmodlem  13906  qusrhm  14084  quscrng  14089  mulgrhm  14165  txbasval  14503  plymullem1  14984  rplogbchbase  15186  sgmmul  15232  lgsdir2  15274  lgsdir  15276  lgsdi  15278  lgsdirnn0  15288  lgsdinn0  15289  lgsquad3  15325