Theorem 3eqtr4rd 2273

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbcnvg  4906  fvco4  5708  phplem4  7024  phplem4on  7037  omp1eomlem  7272  ctssdclemn0  7288  recexnq  7588  prarloclemcalc  7700  addcomprg  7776  mulcomprg  7778  mulcmpblnrlemg  7938  axmulass  8071  divnegap  8864  modqlt  10567  modqmulnn  10576  seq3val  10694  seqvalcd  10695  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1o  10751  bcval5  10997  omgadd  11036  seq3coll  11077  cjreb  11393  recj  11394  imcj  11402  imval2  11421  resqrexlemover  11537  sqrtmul  11562  amgm2  11645  maxabslemab  11733  xrmaxadd  11788  summodclem2a  11908  fsumf1o  11917  sumsnf  11936  sumsplitdc  11959  fsummulc2  11975  binom  12011  bcxmas  12016  expcnvap0  12029  expcnv  12031  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  prodmodclem3  12102  fprodseq  12110  fprodf1o  12115  prodsnf  12119  fprodfac  12142  fprodabs  12143  ege2le3  12198  efaddlem  12201  eftlub  12217  tanval3ap  12241  tannegap  12255  cosmul  12272  cos01bnd  12285  demoivreALT  12301  flodddiv4  12463  dfgcd3  12547  absmulgcd  12554  nninfctlemfo  12577  sqpweven  12713  2sqpwodd  12714  crth  12762  eulerthlema  12768  phisum  12779  pythagtriplem14  12816  pythagtriplem19  12821  pcmul  12840  pcfac  12889  4sqlem12  12941  ctiunctlemfo  13026  setsslnid  13100  qusgrp2  13666  mulgnngsum  13680  mulgnn0gsum  13681  mulgnn0p1  13686  mulgneg  13693  mulgnn0dir  13705  qusghm  13835  gsumfzconst  13894  gsumfzmhm  13896  srgpcomp  13969  opprrng  14056  opprring  14058  oppr1g  14061  invrfvald  14102  rdivmuldivd  14124  lmodvsmmulgdi  14303  lmodsubdi  14324  rmodislmodlem  14330  qusrhm  14508  quscrng  14513  mulgrhm  14589  txbasval  14957  plymullem1  15438  rplogbchbase  15640  sgmmul  15686  lgsdir2  15728  lgsdir  15730  lgsdi  15732  lgsdirnn0  15742  lgsdinn0  15743  lgsquad3  15779  vtxdgop  16052