Theorem 3eqtr4rd 2275

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
2		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr4d 2267	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2267	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  csbcnvg  4914  fvco4  5718  phplem4  7041  phplem4on  7054  omp1eomlem  7293  ctssdclemn0  7309  recexnq  7610  prarloclemcalc  7722  addcomprg  7798  mulcomprg  7800  mulcmpblnrlemg  7960  axmulass  8093  divnegap  8886  modqlt  10596  modqmulnn  10605  seq3val  10723  seqvalcd  10724  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1o  10780  bcval5  11026  omgadd  11066  seq3coll  11107  cjreb  11431  recj  11432  imcj  11440  imval2  11459  resqrexlemover  11575  sqrtmul  11600  amgm2  11683  maxabslemab  11771  xrmaxadd  11826  summodclem2a  11947  fsumf1o  11956  sumsnf  11975  sumsplitdc  11998  fsummulc2  12014  binom  12050  bcxmas  12055  expcnvap0  12068  expcnv  12070  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  prodmodclem3  12141  fprodseq  12149  fprodf1o  12154  prodsnf  12158  fprodfac  12181  fprodabs  12182  ege2le3  12237  efaddlem  12240  eftlub  12256  tanval3ap  12280  tannegap  12294  cosmul  12311  cos01bnd  12324  demoivreALT  12340  flodddiv4  12502  dfgcd3  12586  absmulgcd  12593  nninfctlemfo  12616  sqpweven  12752  2sqpwodd  12753  crth  12801  eulerthlema  12807  phisum  12818  pythagtriplem14  12855  pythagtriplem19  12860  pcmul  12879  pcfac  12928  4sqlem12  12980  ctiunctlemfo  13065  setsslnid  13139  qusgrp2  13705  mulgnngsum  13719  mulgnn0gsum  13720  mulgnn0p1  13725  mulgneg  13732  mulgnn0dir  13744  qusghm  13874  gsumfzconst  13933  gsumfzmhm  13935  gsumsplit0  13938  srgpcomp  14009  opprrng  14096  opprring  14098  oppr1g  14101  invrfvald  14142  rdivmuldivd  14164  lmodvsmmulgdi  14343  lmodsubdi  14364  rmodislmodlem  14370  qusrhm  14548  quscrng  14553  mulgrhm  14629  txbasval  14997  plymullem1  15478  rplogbchbase  15680  sgmmul  15726  lgsdir2  15768  lgsdir  15770  lgsdi  15772  lgsdirnn0  15782  lgsdinn0  15783  lgsquad3  15819  vtxdgop  16149  qdiff  16679  gfsumval  16707  gsumgfsum  16711