Theorem 3eqtr4rd 2249

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 2241	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2241	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  csbcnvg  4862  fvco4  5651  phplem4  6952  phplem4on  6964  omp1eomlem  7196  ctssdclemn0  7212  recexnq  7503  prarloclemcalc  7615  addcomprg  7691  mulcomprg  7693  mulcmpblnrlemg  7853  axmulass  7986  divnegap  8779  modqlt  10478  modqmulnn  10487  seq3val  10605  seqvalcd  10606  seq3caopr3  10636  seqcaopr3g  10637  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seq3f1o  10662  bcval5  10908  omgadd  10947  seq3coll  10987  cjreb  11177  recj  11178  imcj  11186  imval2  11205  resqrexlemover  11321  sqrtmul  11346  amgm2  11429  maxabslemab  11517  xrmaxadd  11572  summodclem2a  11692  fsumf1o  11701  sumsnf  11720  sumsplitdc  11743  fsummulc2  11759  binom  11795  bcxmas  11800  expcnvap0  11813  expcnv  11815  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  prodmodclem3  11886  fprodseq  11894  fprodf1o  11899  prodsnf  11903  fprodfac  11926  fprodabs  11927  ege2le3  11982  efaddlem  11985  eftlub  12001  tanval3ap  12025  tannegap  12039  cosmul  12056  cos01bnd  12069  demoivreALT  12085  flodddiv4  12247  dfgcd3  12331  absmulgcd  12338  nninfctlemfo  12361  sqpweven  12497  2sqpwodd  12498  crth  12546  eulerthlema  12552  phisum  12563  pythagtriplem14  12600  pythagtriplem19  12605  pcmul  12624  pcfac  12673  4sqlem12  12725  ctiunctlemfo  12810  setsslnid  12884  qusgrp2  13449  mulgnngsum  13463  mulgnn0gsum  13464  mulgnn0p1  13469  mulgneg  13476  mulgnn0dir  13488  qusghm  13618  gsumfzconst  13677  gsumfzmhm  13679  srgpcomp  13752  opprrng  13839  opprring  13841  oppr1g  13844  invrfvald  13884  rdivmuldivd  13906  lmodvsmmulgdi  14085  lmodsubdi  14106  rmodislmodlem  14112  qusrhm  14290  quscrng  14295  mulgrhm  14371  txbasval  14739  plymullem1  15220  rplogbchbase  15422  sgmmul  15468  lgsdir2  15510  lgsdir  15512  lgsdi  15514  lgsdirnn0  15524  lgsdinn0  15525  lgsquad3  15561