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  4966  fvco4  5780  phplem4  7160  phplem4on  7173  omp1eomlem  7440  ctssdclemn0  7456  recexnq  7763  prarloclemcalc  7875  addcomprg  7951  mulcomprg  7953  mulcmpblnrlemg  8113  axmulass  8246  divnegap  9044  modqlt  10791  modqmulnn  10800  seq3val  10918  seqvalcd  10919  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1o  10975  bcval5  11223  omgadd  11264  hashmap  11290  seq3coll  11316  s3s4d  11597  s2s5d  11598  s5s2d  11599  cjreb  11653  recj  11654  imcj  11662  imval2  11681  resqrexlemover  11798  sqrtmul  11823  amgm2  11907  maxabslemab  11995  xrmaxadd  12052  summodclem2a  12173  fsumf1o  12182  sumsnf  12201  sumsplitdc  12224  fsummulc2  12240  binom  12276  bcxmas  12281  expcnvap0  12294  expcnv  12296  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  prodmodclem3  12367  fprodseq  12375  fprodf1o  12380  prodsnf  12384  fprodfac  12407  fprodabs  12408  ege2le3  12463  efaddlem  12466  eftlub  12482  tanval3ap  12506  tannegap  12520  cosmul  12537  cos01bnd  12550  demoivreALT  12566  flodddiv4  12728  dfgcd3  12812  absmulgcd  12819  nninfctlemfo  12842  sqpweven  12980  2sqpwodd  12981  crth  13031  eulerthlema  13037  phisum  13048  pythagtriplem14  13085  pythagtriplem19  13090  pcmul  13109  pcfac  13158  4sqlem12  13210  ballotfilemfp1  13289  ballotfilemsf1o  13315  ctiunctlemfo  13388  setsslnid  13462  qusgrp2  13975  mulgnngzsum  13989  mulgnn0gzsum  13990  mulgnn0p1  13995  mulgneg  14002  mulgnn0dir  14014  qusghm  14144  gzsumconst  14233  gzsummhm  14235  gzsumsplit0  14238  gsumvalfi  14242  gzsumgsum  14245  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  srgpcomp  14401  opprrng  14491  opprring  14493  oppr1g  14497  invrfvald  14538  rdivmuldivd  14560  lmodvsmmulgdi  14769  lmodsubdi  14790  rmodislmodlem  14796  qusrhm  14974  quscrng  14979  mulgrhm  15053  asclmulg  15153  txbasval  15493  plymullem1  15974  rplogbchbase  16186  pellexlem2  16230  ppiqfl  16266  sgmmul  16290  chtublem  16295  bposlem9  16319  lgsdir2  16357  lgsdir  16359  lgsdi  16361  lgsdirnn0  16371  lgsdinn0  16372  lgsquad3  16408  vtxdgop  16738  qdiff  17305