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  7040  phplem4on  7053  omp1eomlem  7292  ctssdclemn0  7308  recexnq  7609  prarloclemcalc  7721  addcomprg  7797  mulcomprg  7799  mulcmpblnrlemg  7959  axmulass  8092  divnegap  8885  modqlt  10594  modqmulnn  10603  seq3val  10721  seqvalcd  10722  seq3caopr3  10752  seqcaopr3g  10753  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1o  10778  bcval5  11024  omgadd  11064  seq3coll  11105  cjreb  11426  recj  11427  imcj  11435  imval2  11454  resqrexlemover  11570  sqrtmul  11595  amgm2  11678  maxabslemab  11766  xrmaxadd  11821  summodclem2a  11941  fsumf1o  11950  sumsnf  11969  sumsplitdc  11992  fsummulc2  12008  binom  12044  bcxmas  12049  expcnvap0  12062  expcnv  12064  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  prodmodclem3  12135  fprodseq  12143  fprodf1o  12148  prodsnf  12152  fprodfac  12175  fprodabs  12176  ege2le3  12231  efaddlem  12234  eftlub  12250  tanval3ap  12274  tannegap  12288  cosmul  12305  cos01bnd  12318  demoivreALT  12334  flodddiv4  12496  dfgcd3  12580  absmulgcd  12587  nninfctlemfo  12610  sqpweven  12746  2sqpwodd  12747  crth  12795  eulerthlema  12801  phisum  12812  pythagtriplem14  12849  pythagtriplem19  12854  pcmul  12873  pcfac  12922  4sqlem12  12974  ctiunctlemfo  13059  setsslnid  13133  qusgrp2  13699  mulgnngsum  13713  mulgnn0gsum  13714  mulgnn0p1  13719  mulgneg  13726  mulgnn0dir  13738  qusghm  13868  gsumfzconst  13927  gsumfzmhm  13929  srgpcomp  14002  opprrng  14089  opprring  14091  oppr1g  14094  invrfvald  14135  rdivmuldivd  14157  lmodvsmmulgdi  14336  lmodsubdi  14357  rmodislmodlem  14363  qusrhm  14541  quscrng  14546  mulgrhm  14622  txbasval  14990  plymullem1  15471  rplogbchbase  15673  sgmmul  15719  lgsdir2  15761  lgsdir  15763  lgsdi  15765  lgsdirnn0  15775  lgsdinn0  15776  lgsquad3  15812  vtxdgop  16142  gfsumval  16680  gsumgfsum  16684