Theorem 3eqtr4rd 2251

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  csbcnvg  4880  fvco4  5674  phplem4  6977  phplem4on  6990  omp1eomlem  7222  ctssdclemn0  7238  recexnq  7538  prarloclemcalc  7650  addcomprg  7726  mulcomprg  7728  mulcmpblnrlemg  7888  axmulass  8021  divnegap  8814  modqlt  10515  modqmulnn  10524  seq3val  10642  seqvalcd  10643  seq3caopr3  10673  seqcaopr3g  10674  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1o  10699  bcval5  10945  omgadd  10984  seq3coll  11024  cjreb  11292  recj  11293  imcj  11301  imval2  11320  resqrexlemover  11436  sqrtmul  11461  amgm2  11544  maxabslemab  11632  xrmaxadd  11687  summodclem2a  11807  fsumf1o  11816  sumsnf  11835  sumsplitdc  11858  fsummulc2  11874  binom  11910  bcxmas  11915  expcnvap0  11928  expcnv  11930  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  prodmodclem3  12001  fprodseq  12009  fprodf1o  12014  prodsnf  12018  fprodfac  12041  fprodabs  12042  ege2le3  12097  efaddlem  12100  eftlub  12116  tanval3ap  12140  tannegap  12154  cosmul  12171  cos01bnd  12184  demoivreALT  12200  flodddiv4  12362  dfgcd3  12446  absmulgcd  12453  nninfctlemfo  12476  sqpweven  12612  2sqpwodd  12613  crth  12661  eulerthlema  12667  phisum  12678  pythagtriplem14  12715  pythagtriplem19  12720  pcmul  12739  pcfac  12788  4sqlem12  12840  ctiunctlemfo  12925  setsslnid  12999  qusgrp2  13564  mulgnngsum  13578  mulgnn0gsum  13579  mulgnn0p1  13584  mulgneg  13591  mulgnn0dir  13603  qusghm  13733  gsumfzconst  13792  gsumfzmhm  13794  srgpcomp  13867  opprrng  13954  opprring  13956  oppr1g  13959  invrfvald  13999  rdivmuldivd  14021  lmodvsmmulgdi  14200  lmodsubdi  14221  rmodislmodlem  14227  qusrhm  14405  quscrng  14410  mulgrhm  14486  txbasval  14854  plymullem1  15335  rplogbchbase  15537  sgmmul  15583  lgsdir2  15625  lgsdir  15627  lgsdi  15629  lgsdirnn0  15639  lgsdinn0  15640  lgsquad3  15676