Theorem 3eqtr4rd 2276

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

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

This theorem is referenced by:  csbcnvg  4939  fvco4  5749  phplem4  7109  phplem4on  7122  omp1eomlem  7385  ctssdclemn0  7401  recexnq  7705  prarloclemcalc  7817  addcomprg  7893  mulcomprg  7895  mulcmpblnrlemg  8055  axmulass  8188  divnegap  8980  modqlt  10695  modqmulnn  10704  seq3val  10822  seqvalcd  10823  seq3caopr3  10853  seqcaopr3g  10854  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seq3f1o  10879  bcval5  11125  omgadd  11166  hashmap  11192  seq3coll  11214  s3s4d  11495  s2s5d  11496  s5s2d  11497  cjreb  11551  recj  11552  imcj  11560  imval2  11579  resqrexlemover  11695  sqrtmul  11720  amgm2  11803  maxabslemab  11891  xrmaxadd  11946  summodclem2a  12067  fsumf1o  12076  sumsnf  12095  sumsplitdc  12118  fsummulc2  12134  binom  12170  bcxmas  12175  expcnvap0  12188  expcnv  12190  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  prodmodclem3  12261  fprodseq  12269  fprodf1o  12274  prodsnf  12278  fprodfac  12301  fprodabs  12302  ege2le3  12357  efaddlem  12360  eftlub  12376  tanval3ap  12400  tannegap  12414  cosmul  12431  cos01bnd  12444  demoivreALT  12460  flodddiv4  12622  dfgcd3  12706  absmulgcd  12713  nninfctlemfo  12736  sqpweven  12872  2sqpwodd  12873  crth  12921  eulerthlema  12927  phisum  12938  pythagtriplem14  12975  pythagtriplem19  12980  pcmul  12999  pcfac  13048  4sqlem12  13100  ctiunctlemfo  13190  setsslnid  13264  qusgrp2  13830  mulgnngsum  13844  mulgnn0gsum  13845  mulgnn0p1  13850  mulgneg  13857  mulgnn0dir  13869  qusghm  13999  gsumfzconst  14058  gsumfzmhm  14060  gsumsplit0  14063  srgpcomp  14134  opprrng  14221  opprring  14223  oppr1g  14226  invrfvald  14267  rdivmuldivd  14289  lmodvsmmulgdi  14471  lmodsubdi  14492  rmodislmodlem  14498  qusrhm  14676  quscrng  14681  mulgrhm  14757  txbasval  15132  plymullem1  15613  rplogbchbase  15815  pellexlem2  15846  sgmmul  15864  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsdirnn0  15920  lgsdinn0  15921  lgsquad3  15957  vtxdgop  16287  qdiff  16833  gfsumval  16862  gsumgfsum  16866