Theorem 3eqtr4rd 2132

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

Syntax hints:   -> wi 4   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082

This theorem is referenced by:  csbcnvg  4635  fvco4  5391  phplem4  6627  phplem4on  6639  recexnq  7012  prarloclemcalc  7124  addcomprg  7200  mulcomprg  7202  mulcmpblnrlemg  7349  axmulass  7471  divnegap  8236  modqlt  9803  modqmulnn  9812  iseqvalt  9936  seq3val  9937  iseqcaopr3  9973  seq3f1olemqsumkj  9990  seq3f1olemqsumk  9991  seq3f1olemqsum  9992  seq3f1o  9996  ibcval5  10234  omgadd  10273  iseqcoll  10310  cjreb  10363  recj  10364  imcj  10372  imval2  10391  resqrexlemover  10506  sqrtmul  10531  amgm2  10614  maxabslemab  10702  isummolem2a  10834  fsumf1o  10845  sumsnf  10866  sumsplitdc  10889  fsummulc2  10905  binom  10941  bcxmas  10946  expcnvap0  10959  expcnv  10961  cvgratnnlemnexp  10981  cvgratnnlemmn  10982  ege2le3  11024  efaddlem  11027  eftlub  11043  tanval3ap  11068  tannegap  11082  cosmul  11099  cos01bnd  11112  demoivreALT  11126  flodddiv4  11275  dfgcd3  11340  absmulgcd  11347  sqpweven  11494  2sqpwodd  11495  crth  11541  setsslnid  11608