Theorem 3eqtr4rd 2240

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 2232	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2232	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbcnvg  4851  fvco4  5636  phplem4  6925  phplem4on  6937  omp1eomlem  7169  ctssdclemn0  7185  recexnq  7476  prarloclemcalc  7588  addcomprg  7664  mulcomprg  7666  mulcmpblnrlemg  7826  axmulass  7959  divnegap  8752  modqlt  10444  modqmulnn  10453  seq3val  10571  seqvalcd  10572  seq3caopr3  10602  seqcaopr3g  10603  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1o  10628  bcval5  10874  omgadd  10913  seq3coll  10953  cjreb  11050  recj  11051  imcj  11059  imval2  11078  resqrexlemover  11194  sqrtmul  11219  amgm2  11302  maxabslemab  11390  xrmaxadd  11445  summodclem2a  11565  fsumf1o  11574  sumsnf  11593  sumsplitdc  11616  fsummulc2  11632  binom  11668  bcxmas  11673  expcnvap0  11686  expcnv  11688  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  prodmodclem3  11759  fprodseq  11767  fprodf1o  11772  prodsnf  11776  fprodfac  11799  fprodabs  11800  ege2le3  11855  efaddlem  11858  eftlub  11874  tanval3ap  11898  tannegap  11912  cosmul  11929  cos01bnd  11942  demoivreALT  11958  flodddiv4  12120  dfgcd3  12204  absmulgcd  12211  nninfctlemfo  12234  sqpweven  12370  2sqpwodd  12371  crth  12419  eulerthlema  12425  phisum  12436  pythagtriplem14  12473  pythagtriplem19  12478  pcmul  12497  pcfac  12546  4sqlem12  12598  ctiunctlemfo  12683  setsslnid  12757  qusgrp2  13321  mulgnngsum  13335  mulgnn0gsum  13336  mulgnn0p1  13341  mulgneg  13348  mulgnn0dir  13360  qusghm  13490  gsumfzconst  13549  gsumfzmhm  13551  srgpcomp  13624  opprrng  13711  opprring  13713  oppr1g  13716  invrfvald  13756  rdivmuldivd  13778  lmodvsmmulgdi  13957  lmodsubdi  13978  rmodislmodlem  13984  qusrhm  14162  quscrng  14167  mulgrhm  14243  txbasval  14611  plymullem1  15092  rplogbchbase  15294  sgmmul  15340  lgsdir2  15382  lgsdir  15384  lgsdi  15386  lgsdirnn0  15396  lgsdinn0  15397  lgsquad3  15433