Theorem 3eqtr4rd 2278

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  csbcnvg  4944  fvco4  5754  phplem4  7122  phplem4on  7135  omp1eomlem  7398  ctssdclemn0  7414  recexnq  7721  prarloclemcalc  7833  addcomprg  7909  mulcomprg  7911  mulcmpblnrlemg  8071  axmulass  8204  divnegap  8997  modqlt  10719  modqmulnn  10728  seq3val  10846  seqvalcd  10847  seq3caopr3  10877  seqcaopr3g  10878  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1o  10903  bcval5  11150  omgadd  11191  hashmap  11217  seq3coll  11239  s3s4d  11520  s2s5d  11521  s5s2d  11522  cjreb  11576  recj  11577  imcj  11585  imval2  11604  resqrexlemover  11720  sqrtmul  11745  amgm2  11828  maxabslemab  11916  xrmaxadd  11971  summodclem2a  12092  fsumf1o  12101  sumsnf  12120  sumsplitdc  12143  fsummulc2  12159  binom  12195  bcxmas  12200  expcnvap0  12213  expcnv  12215  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  prodmodclem3  12286  fprodseq  12294  fprodf1o  12299  prodsnf  12303  fprodfac  12326  fprodabs  12327  ege2le3  12382  efaddlem  12385  eftlub  12401  tanval3ap  12425  tannegap  12439  cosmul  12456  cos01bnd  12469  demoivreALT  12485  flodddiv4  12647  dfgcd3  12731  absmulgcd  12738  nninfctlemfo  12761  sqpweven  12897  2sqpwodd  12898  crth  12946  eulerthlema  12952  phisum  12963  pythagtriplem14  13000  pythagtriplem19  13005  pcmul  13024  pcfac  13073  4sqlem12  13125  ballotfilemfp1  13175  ballotfilemsf1o  13201  ctiunctlemfo  13274  setsslnid  13348  qusgrp2  13866  mulgnngsum  13880  mulgnn0gsum  13881  mulgnn0p1  13886  mulgneg  13893  mulgnn0dir  13905  qusghm  14035  gsumfzconst  14094  gsumfzmhm  14096  gsumsplit0  14099  gfsumval  14102  gsumgfsum  14106  srgpcomp  14233  opprrng  14320  opprring  14322  oppr1g  14326  invrfvald  14367  rdivmuldivd  14389  lmodvsmmulgdi  14597  lmodsubdi  14618  rmodislmodlem  14624  qusrhm  14802  quscrng  14807  mulgrhm  14883  txbasval  15258  plymullem1  15739  rplogbchbase  15941  pellexlem2  15972  sgmmul  15990  lgsdir2  16032  lgsdir  16034  lgsdi  16036  lgsdirnn0  16046  lgsdinn0  16047  lgsquad3  16083  vtxdgop  16413  qdiff  16959