Theorem 3eqtr4rd 2282

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  csbcnvg  4964  fvco4  5777  phplem4  7156  phplem4on  7169  omp1eomlem  7434  ctssdclemn0  7450  recexnq  7757  prarloclemcalc  7869  addcomprg  7945  mulcomprg  7947  mulcmpblnrlemg  8107  axmulass  8240  divnegap  9036  modqlt  10770  modqmulnn  10779  seq3val  10897  seqvalcd  10898  seq3caopr3  10928  seqcaopr3g  10929  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seq3f1o  10954  bcval5  11201  omgadd  11242  hashmap  11268  seq3coll  11294  s3s4d  11575  s2s5d  11576  s5s2d  11577  cjreb  11631  recj  11632  imcj  11640  imval2  11659  resqrexlemover  11776  sqrtmul  11801  amgm2  11884  maxabslemab  11972  xrmaxadd  12027  summodclem2a  12148  fsumf1o  12157  sumsnf  12176  sumsplitdc  12199  fsummulc2  12215  binom  12251  bcxmas  12256  expcnvap0  12269  expcnv  12271  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  prodmodclem3  12342  fprodseq  12350  fprodf1o  12355  prodsnf  12359  fprodfac  12382  fprodabs  12383  ege2le3  12438  efaddlem  12441  eftlub  12457  tanval3ap  12481  tannegap  12495  cosmul  12512  cos01bnd  12525  demoivreALT  12541  flodddiv4  12703  dfgcd3  12787  absmulgcd  12794  nninfctlemfo  12817  sqpweven  12953  2sqpwodd  12954  crth  13002  eulerthlema  13008  phisum  13019  pythagtriplem14  13056  pythagtriplem19  13061  pcmul  13080  pcfac  13129  4sqlem12  13181  ballotfilemfp1  13231  ballotfilemsf1o  13257  ctiunctlemfo  13330  setsslnid  13404  qusgrp2  13916  mulgnngzsum  13930  mulgnn0gzsum  13931  mulgnn0p1  13936  mulgneg  13943  mulgnn0dir  13955  qusghm  14085  gzsumconst  14143  gzsummhm  14145  gzsumsplit0  14148  gsumvalfi  14152  gzsumgsum  14155  gsummptfidmadd  14161  srgpcomp  14294  opprrng  14382  opprring  14384  oppr1g  14388  invrfvald  14429  rdivmuldivd  14451  lmodvsmmulgdi  14660  lmodsubdi  14681  rmodislmodlem  14687  qusrhm  14865  quscrng  14870  mulgrhm  14944  asclmulg  15044  txbasval  15368  plymullem1  15849  rplogbchbase  16052  pellexlem2  16092  sgmmul  16110  lgsdir2  16152  lgsdir  16154  lgsdi  16156  lgsdirnn0  16166  lgsdinn0  16167  lgsquad3  16203  vtxdgop  16533  qdiff  17098