Theorem 3eqtr4rd 2273

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 2265	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2265	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbcnvg  4912  fvco4  5714  phplem4  7036  phplem4on  7049  omp1eomlem  7284  ctssdclemn0  7300  recexnq  7600  prarloclemcalc  7712  addcomprg  7788  mulcomprg  7790  mulcmpblnrlemg  7950  axmulass  8083  divnegap  8876  modqlt  10585  modqmulnn  10594  seq3val  10712  seqvalcd  10713  seq3caopr3  10743  seqcaopr3g  10744  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1o  10769  bcval5  11015  omgadd  11055  seq3coll  11096  cjreb  11417  recj  11418  imcj  11426  imval2  11445  resqrexlemover  11561  sqrtmul  11586  amgm2  11669  maxabslemab  11757  xrmaxadd  11812  summodclem2a  11932  fsumf1o  11941  sumsnf  11960  sumsplitdc  11983  fsummulc2  11999  binom  12035  bcxmas  12040  expcnvap0  12053  expcnv  12055  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  prodmodclem3  12126  fprodseq  12134  fprodf1o  12139  prodsnf  12143  fprodfac  12166  fprodabs  12167  ege2le3  12222  efaddlem  12225  eftlub  12241  tanval3ap  12265  tannegap  12279  cosmul  12296  cos01bnd  12309  demoivreALT  12325  flodddiv4  12487  dfgcd3  12571  absmulgcd  12578  nninfctlemfo  12601  sqpweven  12737  2sqpwodd  12738  crth  12786  eulerthlema  12792  phisum  12803  pythagtriplem14  12840  pythagtriplem19  12845  pcmul  12864  pcfac  12913  4sqlem12  12965  ctiunctlemfo  13050  setsslnid  13124  qusgrp2  13690  mulgnngsum  13704  mulgnn0gsum  13705  mulgnn0p1  13710  mulgneg  13717  mulgnn0dir  13729  qusghm  13859  gsumfzconst  13918  gsumfzmhm  13920  srgpcomp  13993  opprrng  14080  opprring  14082  oppr1g  14085  invrfvald  14126  rdivmuldivd  14148  lmodvsmmulgdi  14327  lmodsubdi  14348  rmodislmodlem  14354  qusrhm  14532  quscrng  14537  mulgrhm  14613  txbasval  14981  plymullem1  15462  rplogbchbase  15664  sgmmul  15710  lgsdir2  15752  lgsdir  15754  lgsdi  15756  lgsdirnn0  15766  lgsdinn0  15767  lgsquad3  15803  vtxdgop  16098