Theorem 3eqtr4rd 2214

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  csbcnvg  4795  fvco4  5568  phplem4  6833  phplem4on  6845  omp1eomlem  7071  ctssdclemn0  7087  recexnq  7352  prarloclemcalc  7464  addcomprg  7540  mulcomprg  7542  mulcmpblnrlemg  7702  axmulass  7835  divnegap  8623  modqlt  10289  modqmulnn  10298  seq3val  10414  seqvalcd  10415  seq3caopr3  10437  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1o  10460  bcval5  10697  omgadd  10737  seq3coll  10777  cjreb  10830  recj  10831  imcj  10839  imval2  10858  resqrexlemover  10974  sqrtmul  10999  amgm2  11082  maxabslemab  11170  xrmaxadd  11224  summodclem2a  11344  fsumf1o  11353  sumsnf  11372  sumsplitdc  11395  fsummulc2  11411  binom  11447  bcxmas  11452  expcnvap0  11465  expcnv  11467  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  prodmodclem3  11538  fprodseq  11546  fprodf1o  11551  prodsnf  11555  fprodfac  11578  fprodabs  11579  ege2le3  11634  efaddlem  11637  eftlub  11653  tanval3ap  11677  tannegap  11691  cosmul  11708  cos01bnd  11721  demoivreALT  11736  flodddiv4  11893  dfgcd3  11965  absmulgcd  11972  sqpweven  12129  2sqpwodd  12130  crth  12178  eulerthlema  12184  phisum  12194  pythagtriplem14  12231  pythagtriplem19  12236  pcmul  12255  pcfac  12302  ctiunctlemfo  12394  setsslnid  12467  txbasval  13061  rplogbchbase  13662  lgsdir2  13728  lgsdir  13730  lgsdi  13732  lgsdirnn0  13742  lgsdinn0  13743