Theorem 3eqtr4rd 2233

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

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  csbcnvg  4829  fvco4  5608  phplem4  6882  phplem4on  6894  omp1eomlem  7122  ctssdclemn0  7138  recexnq  7418  prarloclemcalc  7530  addcomprg  7606  mulcomprg  7608  mulcmpblnrlemg  7768  axmulass  7901  divnegap  8692  modqlt  10363  modqmulnn  10372  seq3val  10488  seqvalcd  10489  seq3caopr3  10511  seq3f1olemqsumkj  10528  seq3f1olemqsumk  10529  seq3f1olemqsum  10530  seq3f1o  10534  bcval5  10774  omgadd  10813  seq3coll  10853  cjreb  10906  recj  10907  imcj  10915  imval2  10934  resqrexlemover  11050  sqrtmul  11075  amgm2  11158  maxabslemab  11246  xrmaxadd  11300  summodclem2a  11420  fsumf1o  11429  sumsnf  11448  sumsplitdc  11471  fsummulc2  11487  binom  11523  bcxmas  11528  expcnvap0  11541  expcnv  11543  cvgratnnlemnexp  11563  cvgratnnlemmn  11564  prodmodclem3  11614  fprodseq  11622  fprodf1o  11627  prodsnf  11631  fprodfac  11654  fprodabs  11655  ege2le3  11710  efaddlem  11713  eftlub  11729  tanval3ap  11753  tannegap  11767  cosmul  11784  cos01bnd  11797  demoivreALT  11812  flodddiv4  11970  dfgcd3  12042  absmulgcd  12049  sqpweven  12206  2sqpwodd  12207  crth  12255  eulerthlema  12261  phisum  12271  pythagtriplem14  12308  pythagtriplem19  12313  pcmul  12332  pcfac  12381  4sqlem12  12433  ctiunctlemfo  12489  setsslnid  12563  qusgrp2  13052  mulgnn0p1  13070  mulgneg  13077  mulgnn0dir  13089  qusghm  13218  srgpcomp  13341  opprrng  13424  opprring  13426  oppr1g  13429  invrfvald  13469  rdivmuldivd  13491  lmodvsmmulgdi  13636  lmodsubdi  13657  rmodislmodlem  13663  quscrng  13844  mulgrhm  13904  txbasval  14219  rplogbchbase  14820  lgsdir2  14887  lgsdir  14889  lgsdi  14891  lgsdirnn0  14901  lgsdinn0  14902