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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  csbcnvg  4959  fvco4  5771  phplem4  7146  phplem4on  7159  omp1eomlem  7424  ctssdclemn0  7440  recexnq  7747  prarloclemcalc  7859  addcomprg  7935  mulcomprg  7937  mulcmpblnrlemg  8097  axmulass  8230  divnegap  9026  modqlt  10748  modqmulnn  10757  seq3val  10875  seqvalcd  10876  seq3caopr3  10906  seqcaopr3g  10907  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1o  10932  bcval5  11179  omgadd  11220  hashmap  11246  seq3coll  11272  s3s4d  11553  s2s5d  11554  s5s2d  11555  cjreb  11609  recj  11610  imcj  11618  imval2  11637  resqrexlemover  11754  sqrtmul  11779  amgm2  11862  maxabslemab  11950  xrmaxadd  12005  summodclem2a  12126  fsumf1o  12135  sumsnf  12154  sumsplitdc  12177  fsummulc2  12193  binom  12229  bcxmas  12234  expcnvap0  12247  expcnv  12249  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  prodmodclem3  12320  fprodseq  12328  fprodf1o  12333  prodsnf  12337  fprodfac  12360  fprodabs  12361  ege2le3  12416  efaddlem  12419  eftlub  12435  tanval3ap  12459  tannegap  12473  cosmul  12490  cos01bnd  12503  demoivreALT  12519  flodddiv4  12681  dfgcd3  12765  absmulgcd  12772  nninfctlemfo  12795  sqpweven  12931  2sqpwodd  12932  crth  12980  eulerthlema  12986  phisum  12997  pythagtriplem14  13034  pythagtriplem19  13039  pcmul  13058  pcfac  13107  4sqlem12  13159  ballotfilemfp1  13209  ballotfilemsf1o  13235  ctiunctlemfo  13308  setsslnid  13382  qusgrp2  13893  mulgnngzsum  13907  mulgnn0gzsum  13908  mulgnn0p1  13913  mulgneg  13920  mulgnn0dir  13932  qusghm  14062  gzsumconst  14120  gzsummhm  14122  gzsumsplit0  14125  gsumvalfi  14129  gzsumgsum  14132  gsummptfidmadd  14138  srgpcomp  14268  opprrng  14355  opprring  14357  oppr1g  14361  invrfvald  14402  rdivmuldivd  14424  lmodvsmmulgdi  14632  lmodsubdi  14653  rmodislmodlem  14659  qusrhm  14837  quscrng  14842  mulgrhm  14916  txbasval  15291  plymullem1  15772  rplogbchbase  15975  pellexlem2  16006  sgmmul  16024  lgsdir2  16066  lgsdir  16068  lgsdi  16070  lgsdirnn0  16080  lgsdinn0  16081  lgsquad3  16117  vtxdgop  16447  qdiff  17003