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  9038  modqlt  10783  modqmulnn  10792  seq3val  10910  seqvalcd  10911  seq3caopr3  10941  seqcaopr3g  10942  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1o  10967  bcval5  11215  omgadd  11256  hashmap  11282  seq3coll  11308  s3s4d  11589  s2s5d  11590  s5s2d  11591  cjreb  11645  recj  11646  imcj  11654  imval2  11673  resqrexlemover  11790  sqrtmul  11815  amgm2  11899  maxabslemab  11987  xrmaxadd  12043  summodclem2a  12164  fsumf1o  12173  sumsnf  12192  sumsplitdc  12215  fsummulc2  12231  binom  12267  bcxmas  12272  expcnvap0  12285  expcnv  12287  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  prodmodclem3  12358  fprodseq  12366  fprodf1o  12371  prodsnf  12375  fprodfac  12398  fprodabs  12399  ege2le3  12454  efaddlem  12457  eftlub  12473  tanval3ap  12497  tannegap  12511  cosmul  12528  cos01bnd  12541  demoivreALT  12557  flodddiv4  12719  dfgcd3  12803  absmulgcd  12810  nninfctlemfo  12833  sqpweven  12971  2sqpwodd  12972  crth  13022  eulerthlema  13028  phisum  13039  pythagtriplem14  13076  pythagtriplem19  13081  pcmul  13100  pcfac  13149  4sqlem12  13201  ballotfilemfp1  13280  ballotfilemsf1o  13306  ctiunctlemfo  13379  setsslnid  13453  qusgrp2  13965  mulgnngzsum  13979  mulgnn0gzsum  13980  mulgnn0p1  13985  mulgneg  13992  mulgnn0dir  14004  qusghm  14134  gzsumconst  14192  gzsummhm  14194  gzsumsplit0  14197  gsumvalfi  14201  gzsumgsum  14204  gsummptfidmadd  14210  srgpcomp  14343  opprrng  14431  opprring  14433  oppr1g  14437  invrfvald  14478  rdivmuldivd  14500  lmodvsmmulgdi  14709  lmodsubdi  14730  rmodislmodlem  14736  qusrhm  14914  quscrng  14919  mulgrhm  14993  asclmulg  15093  txbasval  15417  plymullem1  15898  rplogbchbase  16105  pellexlem2  16149  ppiqfl  16172  sgmmul  16191  lgsdir2  16250  lgsdir  16252  lgsdi  16254  lgsdirnn0  16264  lgsdinn0  16265  lgsquad3  16301  vtxdgop  16631  qdiff  17196