Theorem 3eqtr4rd 2273

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbcnvg  4906  fvco4  5706  phplem4  7016  phplem4on  7029  omp1eomlem  7261  ctssdclemn0  7277  recexnq  7577  prarloclemcalc  7689  addcomprg  7765  mulcomprg  7767  mulcmpblnrlemg  7927  axmulass  8060  divnegap  8853  modqlt  10555  modqmulnn  10564  seq3val  10682  seqvalcd  10683  seq3caopr3  10713  seqcaopr3g  10714  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1o  10739  bcval5  10985  omgadd  11024  seq3coll  11064  cjreb  11377  recj  11378  imcj  11386  imval2  11405  resqrexlemover  11521  sqrtmul  11546  amgm2  11629  maxabslemab  11717  xrmaxadd  11772  summodclem2a  11892  fsumf1o  11901  sumsnf  11920  sumsplitdc  11943  fsummulc2  11959  binom  11995  bcxmas  12000  expcnvap0  12013  expcnv  12015  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  prodmodclem3  12086  fprodseq  12094  fprodf1o  12099  prodsnf  12103  fprodfac  12126  fprodabs  12127  ege2le3  12182  efaddlem  12185  eftlub  12201  tanval3ap  12225  tannegap  12239  cosmul  12256  cos01bnd  12269  demoivreALT  12285  flodddiv4  12447  dfgcd3  12531  absmulgcd  12538  nninfctlemfo  12561  sqpweven  12697  2sqpwodd  12698  crth  12746  eulerthlema  12752  phisum  12763  pythagtriplem14  12800  pythagtriplem19  12805  pcmul  12824  pcfac  12873  4sqlem12  12925  ctiunctlemfo  13010  setsslnid  13084  qusgrp2  13650  mulgnngsum  13664  mulgnn0gsum  13665  mulgnn0p1  13670  mulgneg  13677  mulgnn0dir  13689  qusghm  13819  gsumfzconst  13878  gsumfzmhm  13880  srgpcomp  13953  opprrng  14040  opprring  14042  oppr1g  14045  invrfvald  14086  rdivmuldivd  14108  lmodvsmmulgdi  14287  lmodsubdi  14308  rmodislmodlem  14314  qusrhm  14492  quscrng  14497  mulgrhm  14573  txbasval  14941  plymullem1  15422  rplogbchbase  15624  sgmmul  15670  lgsdir2  15712  lgsdir  15714  lgsdi  15716  lgsdirnn0  15726  lgsdinn0  15727  lgsquad3  15763