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  8661  modqlt  10330  modqmulnn  10339  seq3val  10455  seqvalcd  10456  seq3caopr3  10478  seq3f1olemqsumkj  10495  seq3f1olemqsumk  10496  seq3f1olemqsum  10497  seq3f1o  10501  bcval5  10738  omgadd  10777  seq3coll  10817  cjreb  10870  recj  10871  imcj  10879  imval2  10898  resqrexlemover  11014  sqrtmul  11039  amgm2  11122  maxabslemab  11210  xrmaxadd  11264  summodclem2a  11384  fsumf1o  11393  sumsnf  11412  sumsplitdc  11435  fsummulc2  11451  binom  11487  bcxmas  11492  expcnvap0  11505  expcnv  11507  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  prodmodclem3  11578  fprodseq  11586  fprodf1o  11591  prodsnf  11595  fprodfac  11618  fprodabs  11619  ege2le3  11674  efaddlem  11677  eftlub  11693  tanval3ap  11717  tannegap  11731  cosmul  11748  cos01bnd  11761  demoivreALT  11776  flodddiv4  11933  dfgcd3  12005  absmulgcd  12012  sqpweven  12169  2sqpwodd  12170  crth  12218  eulerthlema  12224  phisum  12234  pythagtriplem14  12271  pythagtriplem19  12276  pcmul  12295  pcfac  12342  ctiunctlemfo  12434  setsslnid  12508  mulgnn0p1  12948  mulgneg  12955  mulgnn0dir  12966  srgpcomp  13126  opprring  13202  oppr1g  13205  invrfvald  13244  rdivmuldivd  13266  txbasval  13660  rplogbchbase  14261  lgsdir2  14327  lgsdir  14329  lgsdi  14331  lgsdirnn0  14341  lgsdinn0  14342