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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  csbcnvg  4914  fvco4  5718  phplem4  7041  phplem4on  7054  omp1eomlem  7293  ctssdclemn0  7309  recexnq  7610  prarloclemcalc  7722  addcomprg  7798  mulcomprg  7800  mulcmpblnrlemg  7960  axmulass  8093  divnegap  8886  modqlt  10596  modqmulnn  10605  seq3val  10723  seqvalcd  10724  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1o  10780  bcval5  11026  omgadd  11066  seq3coll  11107  s3s4d  11388  s2s5d  11389  s5s2d  11390  cjreb  11444  recj  11445  imcj  11453  imval2  11472  resqrexlemover  11588  sqrtmul  11613  amgm2  11696  maxabslemab  11784  xrmaxadd  11839  summodclem2a  11960  fsumf1o  11969  sumsnf  11988  sumsplitdc  12011  fsummulc2  12027  binom  12063  bcxmas  12068  expcnvap0  12081  expcnv  12083  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  prodmodclem3  12154  fprodseq  12162  fprodf1o  12167  prodsnf  12171  fprodfac  12194  fprodabs  12195  ege2le3  12250  efaddlem  12253  eftlub  12269  tanval3ap  12293  tannegap  12307  cosmul  12324  cos01bnd  12337  demoivreALT  12353  flodddiv4  12515  dfgcd3  12599  absmulgcd  12606  nninfctlemfo  12629  sqpweven  12765  2sqpwodd  12766  crth  12814  eulerthlema  12820  phisum  12831  pythagtriplem14  12868  pythagtriplem19  12873  pcmul  12892  pcfac  12941  4sqlem12  12993  ctiunctlemfo  13078  setsslnid  13152  qusgrp2  13718  mulgnngsum  13732  mulgnn0gsum  13733  mulgnn0p1  13738  mulgneg  13745  mulgnn0dir  13757  qusghm  13887  gsumfzconst  13946  gsumfzmhm  13948  gsumsplit0  13951  srgpcomp  14022  opprrng  14109  opprring  14111  oppr1g  14114  invrfvald  14155  rdivmuldivd  14177  lmodvsmmulgdi  14356  lmodsubdi  14377  rmodislmodlem  14383  qusrhm  14561  quscrng  14566  mulgrhm  14642  txbasval  15010  plymullem1  15491  rplogbchbase  15693  sgmmul  15739  lgsdir2  15781  lgsdir  15783  lgsdi  15785  lgsdirnn0  15795  lgsdinn0  15796  lgsquad3  15832  vtxdgop  16162  qdiff  16704  gfsumval  16732  gsumgfsum  16736