Theorem 3eqtr4rd 2209

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

Syntax hints:   -> wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  csbcnvg  4787  fvco4  5557  phplem4  6817  phplem4on  6829  omp1eomlem  7055  ctssdclemn0  7071  recexnq  7327  prarloclemcalc  7439  addcomprg  7515  mulcomprg  7517  mulcmpblnrlemg  7677  axmulass  7810  divnegap  8598  modqlt  10264  modqmulnn  10273  seq3val  10389  seqvalcd  10390  seq3caopr3  10412  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1o  10435  bcval5  10672  omgadd  10711  seq3coll  10751  cjreb  10804  recj  10805  imcj  10813  imval2  10832  resqrexlemover  10948  sqrtmul  10973  amgm2  11056  maxabslemab  11144  xrmaxadd  11198  summodclem2a  11318  fsumf1o  11327  sumsnf  11346  sumsplitdc  11369  fsummulc2  11385  binom  11421  bcxmas  11426  expcnvap0  11439  expcnv  11441  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  prodmodclem3  11512  fprodseq  11520  fprodf1o  11525  prodsnf  11529  fprodfac  11552  fprodabs  11553  ege2le3  11608  efaddlem  11611  eftlub  11627  tanval3ap  11651  tannegap  11665  cosmul  11682  cos01bnd  11695  demoivreALT  11710  flodddiv4  11867  dfgcd3  11939  absmulgcd  11946  sqpweven  12103  2sqpwodd  12104  crth  12152  eulerthlema  12158  phisum  12168  pythagtriplem14  12205  pythagtriplem19  12210  pcmul  12229  pcfac  12276  ctiunctlemfo  12368  setsslnid  12441  txbasval  12867  rplogbchbase  13468  lgsdir2  13534  lgsdir  13536  lgsdi  13538  lgsdirnn0  13548  lgsdinn0  13549