Theorem 3eqtr4rd 2221

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  csbcnvg  4811  fvco4  5588  phplem4  6854  phplem4on  6866  omp1eomlem  7092  ctssdclemn0  7108  recexnq  7388  prarloclemcalc  7500  addcomprg  7576  mulcomprg  7578  mulcmpblnrlemg  7738  axmulass  7871  divnegap  8662  modqlt  10332  modqmulnn  10341  seq3val  10457  seqvalcd  10458  seq3caopr3  10480  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1o  10503  bcval5  10742  omgadd  10781  seq3coll  10821  cjreb  10874  recj  10875  imcj  10883  imval2  10902  resqrexlemover  11018  sqrtmul  11043  amgm2  11126  maxabslemab  11214  xrmaxadd  11268  summodclem2a  11388  fsumf1o  11397  sumsnf  11416  sumsplitdc  11439  fsummulc2  11455  binom  11491  bcxmas  11496  expcnvap0  11509  expcnv  11511  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  prodmodclem3  11582  fprodseq  11590  fprodf1o  11595  prodsnf  11599  fprodfac  11622  fprodabs  11623  ege2le3  11678  efaddlem  11681  eftlub  11697  tanval3ap  11721  tannegap  11735  cosmul  11752  cos01bnd  11765  demoivreALT  11780  flodddiv4  11938  dfgcd3  12010  absmulgcd  12017  sqpweven  12174  2sqpwodd  12175  crth  12223  eulerthlema  12229  phisum  12239  pythagtriplem14  12276  pythagtriplem19  12281  pcmul  12300  pcfac  12347  ctiunctlemfo  12439  setsslnid  12513  mulgnn0p1  12993  mulgneg  13000  mulgnn0dir  13011  srgpcomp  13171  opprring  13247  oppr1g  13250  invrfvald  13289  rdivmuldivd  13311  txbasval  13737  rplogbchbase  14338  lgsdir2  14404  lgsdir  14406  lgsdi  14408  lgsdirnn0  14418  lgsdinn0  14419