Theorem 3eqtr4rd 2184

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

Syntax hints:   → wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  csbcnvg  4731  fvco4  5501  phplem4  6757  phplem4on  6769  omp1eomlem  6987  ctssdclemn0  7003  recexnq  7222  prarloclemcalc  7334  addcomprg  7410  mulcomprg  7412  mulcmpblnrlemg  7572  axmulass  7705  divnegap  8490  modqlt  10137  modqmulnn  10146  seq3val  10262  seqvalcd  10263  seq3caopr3  10285  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1o  10308  bcval5  10541  omgadd  10580  seq3coll  10617  cjreb  10670  recj  10671  imcj  10679  imval2  10698  resqrexlemover  10814  sqrtmul  10839  amgm2  10922  maxabslemab  11010  xrmaxadd  11062  summodclem2a  11182  fsumf1o  11191  sumsnf  11210  sumsplitdc  11233  fsummulc2  11249  binom  11285  bcxmas  11290  expcnvap0  11303  expcnv  11305  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  prodmodclem3  11376  fprodseq  11384  ege2le3  11414  efaddlem  11417  eftlub  11433  tanval3ap  11457  tannegap  11471  cosmul  11488  cos01bnd  11501  demoivreALT  11516  flodddiv4  11667  dfgcd3  11734  absmulgcd  11741  sqpweven  11889  2sqpwodd  11890  crth  11936  ctiunctlemfo  11988  setsslnid  12049  txbasval  12475  rplogbchbase  13075