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  4812  fvco4  5589  phplem4  6855  phplem4on  6867  omp1eomlem  7093  ctssdclemn0  7109  recexnq  7389  prarloclemcalc  7501  addcomprg  7577  mulcomprg  7579  mulcmpblnrlemg  7739  axmulass  7872  divnegap  8663  modqlt  10333  modqmulnn  10342  seq3val  10458  seqvalcd  10459  seq3caopr3  10481  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1o  10504  bcval5  10743  omgadd  10782  seq3coll  10822  cjreb  10875  recj  10876  imcj  10884  imval2  10903  resqrexlemover  11019  sqrtmul  11044  amgm2  11127  maxabslemab  11215  xrmaxadd  11269  summodclem2a  11389  fsumf1o  11398  sumsnf  11417  sumsplitdc  11440  fsummulc2  11456  binom  11492  bcxmas  11497  expcnvap0  11510  expcnv  11512  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  prodmodclem3  11583  fprodseq  11591  fprodf1o  11596  prodsnf  11600  fprodfac  11623  fprodabs  11624  ege2le3  11679  efaddlem  11682  eftlub  11698  tanval3ap  11722  tannegap  11736  cosmul  11753  cos01bnd  11766  demoivreALT  11781  flodddiv4  11939  dfgcd3  12011  absmulgcd  12018  sqpweven  12175  2sqpwodd  12176  crth  12224  eulerthlema  12230  phisum  12240  pythagtriplem14  12277  pythagtriplem19  12282  pcmul  12301  pcfac  12348  ctiunctlemfo  12440  setsslnid  12514  mulgnn0p1  12994  mulgneg  13001  mulgnn0dir  13013  srgpcomp  13173  opprring  13249  oppr1g  13252  invrfvald  13291  rdivmuldivd  13313  lmodvsmmulgdi  13413  lmodsubdi  13434  rmodislmodlem  13440  txbasval  13770  rplogbchbase  14371  lgsdir2  14437  lgsdir  14439  lgsdi  14441  lgsdirnn0  14451  lgsdinn0  14452