Theorem 3eqtr4rd 2183

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  csbcnvg  4723  fvco4  5493  phplem4  6749  phplem4on  6761  omp1eomlem  6979  ctssdclemn0  6995  recexnq  7198  prarloclemcalc  7310  addcomprg  7386  mulcomprg  7388  mulcmpblnrlemg  7548  axmulass  7681  divnegap  8466  modqlt  10106  modqmulnn  10115  seq3val  10231  seqvalcd  10232  seq3caopr3  10254  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1o  10277  bcval5  10509  omgadd  10548  seq3coll  10585  cjreb  10638  recj  10639  imcj  10647  imval2  10666  resqrexlemover  10782  sqrtmul  10807  amgm2  10890  maxabslemab  10978  xrmaxadd  11030  summodclem2a  11150  fsumf1o  11159  sumsnf  11178  sumsplitdc  11201  fsummulc2  11217  binom  11253  bcxmas  11258  expcnvap0  11271  expcnv  11273  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  prodmodclem3  11344  ege2le3  11377  efaddlem  11380  eftlub  11396  tanval3ap  11421  tannegap  11435  cosmul  11452  cos01bnd  11465  demoivreALT  11480  flodddiv4  11631  dfgcd3  11698  absmulgcd  11705  sqpweven  11853  2sqpwodd  11854  crth  11900  ctiunctlemfo  11952  setsslnid  12010  txbasval  12436