Theorem 3eqtr4rd 2240

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 2232	. 2 |- ( ph -> D = A )
4		3eqtr4d.2	. 2 |- ( ph -> C = A )
5	3, 4	eqtr4d 2232	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbcnvg  4851  fvco4  5636  phplem4  6925  phplem4on  6937  omp1eomlem  7169  ctssdclemn0  7185  recexnq  7474  prarloclemcalc  7586  addcomprg  7662  mulcomprg  7664  mulcmpblnrlemg  7824  axmulass  7957  divnegap  8750  modqlt  10442  modqmulnn  10451  seq3val  10569  seqvalcd  10570  seq3caopr3  10600  seqcaopr3g  10601  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1o  10626  bcval5  10872  omgadd  10911  seq3coll  10951  cjreb  11048  recj  11049  imcj  11057  imval2  11076  resqrexlemover  11192  sqrtmul  11217  amgm2  11300  maxabslemab  11388  xrmaxadd  11443  summodclem2a  11563  fsumf1o  11572  sumsnf  11591  sumsplitdc  11614  fsummulc2  11630  binom  11666  bcxmas  11671  expcnvap0  11684  expcnv  11686  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  prodmodclem3  11757  fprodseq  11765  fprodf1o  11770  prodsnf  11774  fprodfac  11797  fprodabs  11798  ege2le3  11853  efaddlem  11856  eftlub  11872  tanval3ap  11896  tannegap  11910  cosmul  11927  cos01bnd  11940  demoivreALT  11956  flodddiv4  12118  dfgcd3  12202  absmulgcd  12209  nninfctlemfo  12232  sqpweven  12368  2sqpwodd  12369  crth  12417  eulerthlema  12423  phisum  12434  pythagtriplem14  12471  pythagtriplem19  12476  pcmul  12495  pcfac  12544  4sqlem12  12596  ctiunctlemfo  12681  setsslnid  12755  qusgrp2  13319  mulgnngsum  13333  mulgnn0gsum  13334  mulgnn0p1  13339  mulgneg  13346  mulgnn0dir  13358  qusghm  13488  gsumfzconst  13547  gsumfzmhm  13549  srgpcomp  13622  opprrng  13709  opprring  13711  oppr1g  13714  invrfvald  13754  rdivmuldivd  13776  lmodvsmmulgdi  13955  lmodsubdi  13976  rmodislmodlem  13982  qusrhm  14160  quscrng  14165  mulgrhm  14241  txbasval  14587  plymullem1  15068  rplogbchbase  15270  sgmmul  15316  lgsdir2  15358  lgsdir  15360  lgsdi  15362  lgsdirnn0  15372  lgsdinn0  15373  lgsquad3  15409