Theorem 3eqtr4rd 2237

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  csbcnvg  4847  fvco4  5630  phplem4  6913  phplem4on  6925  omp1eomlem  7155  ctssdclemn0  7171  recexnq  7452  prarloclemcalc  7564  addcomprg  7640  mulcomprg  7642  mulcmpblnrlemg  7802  axmulass  7935  divnegap  8727  modqlt  10407  modqmulnn  10416  seq3val  10534  seqvalcd  10535  seq3caopr3  10565  seqcaopr3g  10566  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1o  10591  bcval5  10837  omgadd  10876  seq3coll  10916  cjreb  11013  recj  11014  imcj  11022  imval2  11041  resqrexlemover  11157  sqrtmul  11182  amgm2  11265  maxabslemab  11353  xrmaxadd  11407  summodclem2a  11527  fsumf1o  11536  sumsnf  11555  sumsplitdc  11578  fsummulc2  11594  binom  11630  bcxmas  11635  expcnvap0  11648  expcnv  11650  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  prodmodclem3  11721  fprodseq  11729  fprodf1o  11734  prodsnf  11738  fprodfac  11761  fprodabs  11762  ege2le3  11817  efaddlem  11820  eftlub  11836  tanval3ap  11860  tannegap  11874  cosmul  11891  cos01bnd  11904  demoivreALT  11920  flodddiv4  12078  dfgcd3  12150  absmulgcd  12157  nninfctlemfo  12180  sqpweven  12316  2sqpwodd  12317  crth  12365  eulerthlema  12371  phisum  12381  pythagtriplem14  12418  pythagtriplem19  12423  pcmul  12442  pcfac  12491  4sqlem12  12543  ctiunctlemfo  12599  setsslnid  12673  qusgrp2  13186  mulgnngsum  13200  mulgnn0gsum  13201  mulgnn0p1  13206  mulgneg  13213  mulgnn0dir  13225  qusghm  13355  gsumfzconst  13414  gsumfzmhm  13416  srgpcomp  13489  opprrng  13576  opprring  13578  oppr1g  13581  invrfvald  13621  rdivmuldivd  13643  lmodvsmmulgdi  13822  lmodsubdi  13843  rmodislmodlem  13849  qusrhm  14027  quscrng  14032  mulgrhm  14108  txbasval  14446  plymullem1  14927  rplogbchbase  15123  lgsdir2  15190  lgsdir  15192  lgsdi  15194  lgsdirnn0  15204  lgsdinn0  15205  lgsquad3  15241