Theorem 3eqtr4rd 2275

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  csbcnvg  4920  fvco4  5727  phplem4  7084  phplem4on  7097  omp1eomlem  7353  ctssdclemn0  7369  recexnq  7670  prarloclemcalc  7782  addcomprg  7858  mulcomprg  7860  mulcmpblnrlemg  8020  axmulass  8153  divnegap  8945  modqlt  10658  modqmulnn  10667  seq3val  10785  seqvalcd  10786  seq3caopr3  10816  seqcaopr3g  10817  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seq3f1o  10842  bcval5  11088  omgadd  11128  seq3coll  11169  s3s4d  11450  s2s5d  11451  s5s2d  11452  cjreb  11506  recj  11507  imcj  11515  imval2  11534  resqrexlemover  11650  sqrtmul  11675  amgm2  11758  maxabslemab  11846  xrmaxadd  11901  summodclem2a  12022  fsumf1o  12031  sumsnf  12050  sumsplitdc  12073  fsummulc2  12089  binom  12125  bcxmas  12130  expcnvap0  12143  expcnv  12145  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  prodmodclem3  12216  fprodseq  12224  fprodf1o  12229  prodsnf  12233  fprodfac  12256  fprodabs  12257  ege2le3  12312  efaddlem  12315  eftlub  12331  tanval3ap  12355  tannegap  12369  cosmul  12386  cos01bnd  12399  demoivreALT  12415  flodddiv4  12577  dfgcd3  12661  absmulgcd  12668  nninfctlemfo  12691  sqpweven  12827  2sqpwodd  12828  crth  12876  eulerthlema  12882  phisum  12893  pythagtriplem14  12930  pythagtriplem19  12935  pcmul  12954  pcfac  13003  4sqlem12  13055  ctiunctlemfo  13140  setsslnid  13214  qusgrp2  13780  mulgnngsum  13794  mulgnn0gsum  13795  mulgnn0p1  13800  mulgneg  13807  mulgnn0dir  13819  qusghm  13949  gsumfzconst  14008  gsumfzmhm  14010  gsumsplit0  14013  srgpcomp  14084  opprrng  14171  opprring  14173  oppr1g  14176  invrfvald  14217  rdivmuldivd  14239  lmodvsmmulgdi  14419  lmodsubdi  14440  rmodislmodlem  14446  qusrhm  14624  quscrng  14629  mulgrhm  14705  txbasval  15078  plymullem1  15559  rplogbchbase  15761  pellexlem2  15792  sgmmul  15810  lgsdir2  15852  lgsdir  15854  lgsdi  15856  lgsdirnn0  15866  lgsdinn0  15867  lgsquad3  15903  vtxdgop  16233  qdiff  16781  gfsumval  16809  gsumgfsum  16813