Theorem 3eqtr4rd 2219

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

Syntax hints:   -> wi 4   = wceq 1353

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  csbcnvg  4804  fvco4  5580  phplem4  6845  phplem4on  6857  omp1eomlem  7083  ctssdclemn0  7099  recexnq  7364  prarloclemcalc  7476  addcomprg  7552  mulcomprg  7554  mulcmpblnrlemg  7714  axmulass  7847  divnegap  8636  modqlt  10303  modqmulnn  10312  seq3val  10428  seqvalcd  10429  seq3caopr3  10451  seq3f1olemqsumkj  10468  seq3f1olemqsumk  10469  seq3f1olemqsum  10470  seq3f1o  10474  bcval5  10711  omgadd  10750  seq3coll  10790  cjreb  10843  recj  10844  imcj  10852  imval2  10871  resqrexlemover  10987  sqrtmul  11012  amgm2  11095  maxabslemab  11183  xrmaxadd  11237  summodclem2a  11357  fsumf1o  11366  sumsnf  11385  sumsplitdc  11408  fsummulc2  11424  binom  11460  bcxmas  11465  expcnvap0  11478  expcnv  11480  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  prodmodclem3  11551  fprodseq  11559  fprodf1o  11564  prodsnf  11568  fprodfac  11591  fprodabs  11592  ege2le3  11647  efaddlem  11650  eftlub  11666  tanval3ap  11690  tannegap  11704  cosmul  11721  cos01bnd  11734  demoivreALT  11749  flodddiv4  11906  dfgcd3  11978  absmulgcd  11985  sqpweven  12142  2sqpwodd  12143  crth  12191  eulerthlema  12197  phisum  12207  pythagtriplem14  12244  pythagtriplem19  12249  pcmul  12268  pcfac  12315  ctiunctlemfo  12407  setsslnid  12480  mulgnn0p1  12864  mulgneg  12871  mulgnn0dir  12882  srgpcomp  12979  opprring  13053  oppr1g  13056  txbasval  13347  rplogbchbase  13948  lgsdir2  14014  lgsdir  14016  lgsdi  14018  lgsdirnn0  14028  lgsdinn0  14029