Theorem 3eqtr4rd 2237

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 2229	. 2 |- ( ph -> D = A )
4		3eqtr4d.2	. 2 |- ( ph -> C = A )
5	3, 4	eqtr4d 2229	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  csbcnvg  4846  fvco4  5629  phplem4  6911  phplem4on  6923  omp1eomlem  7153  ctssdclemn0  7169  recexnq  7450  prarloclemcalc  7562  addcomprg  7638  mulcomprg  7640  mulcmpblnrlemg  7800  axmulass  7933  divnegap  8725  modqlt  10404  modqmulnn  10413  seq3val  10531  seqvalcd  10532  seq3caopr3  10562  seqcaopr3g  10563  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1o  10588  bcval5  10834  omgadd  10873  seq3coll  10913  cjreb  11010  recj  11011  imcj  11019  imval2  11038  resqrexlemover  11154  sqrtmul  11179  amgm2  11262  maxabslemab  11350  xrmaxadd  11404  summodclem2a  11524  fsumf1o  11533  sumsnf  11552  sumsplitdc  11575  fsummulc2  11591  binom  11627  bcxmas  11632  expcnvap0  11645  expcnv  11647  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  prodmodclem3  11718  fprodseq  11726  fprodf1o  11731  prodsnf  11735  fprodfac  11758  fprodabs  11759  ege2le3  11814  efaddlem  11817  eftlub  11833  tanval3ap  11857  tannegap  11871  cosmul  11888  cos01bnd  11901  demoivreALT  11917  flodddiv4  12075  dfgcd3  12147  absmulgcd  12154  nninfctlemfo  12177  sqpweven  12313  2sqpwodd  12314  crth  12362  eulerthlema  12368  phisum  12378  pythagtriplem14  12415  pythagtriplem19  12420  pcmul  12439  pcfac  12488  4sqlem12  12540  ctiunctlemfo  12596  setsslnid  12670  qusgrp2  13183  mulgnngsum  13197  mulgnn0gsum  13198  mulgnn0p1  13203  mulgneg  13210  mulgnn0dir  13222  qusghm  13352  gsumfzconst  13411  gsumfzmhm  13413  srgpcomp  13486  opprrng  13573  opprring  13575  oppr1g  13578  invrfvald  13618  rdivmuldivd  13640  lmodvsmmulgdi  13819  lmodsubdi  13840  rmodislmodlem  13846  qusrhm  14024  quscrng  14029  mulgrhm  14097  txbasval  14435  plymullem1  14894  rplogbchbase  15082  lgsdir2  15149  lgsdir  15151  lgsdi  15153  lgsdirnn0  15163  lgsdinn0  15164