Theorem 3eqtr4rd 2282

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  csbcnvg  4964  fvco4  5777  phplem4  7156  phplem4on  7169  omp1eomlem  7435  ctssdclemn0  7451  recexnq  7758  prarloclemcalc  7870  addcomprg  7946  mulcomprg  7948  mulcmpblnrlemg  8108  axmulass  8241  divnegap  9039  modqlt  10785  modqmulnn  10794  seq3val  10912  seqvalcd  10913  seq3caopr3  10943  seqcaopr3g  10944  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1o  10969  bcval5  11217  omgadd  11258  hashmap  11284  seq3coll  11310  s3s4d  11591  s2s5d  11592  s5s2d  11593  cjreb  11647  recj  11648  imcj  11656  imval2  11675  resqrexlemover  11792  sqrtmul  11817  amgm2  11901  maxabslemab  11989  xrmaxadd  12046  summodclem2a  12167  fsumf1o  12176  sumsnf  12195  sumsplitdc  12218  fsummulc2  12234  binom  12270  bcxmas  12275  expcnvap0  12288  expcnv  12290  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  prodmodclem3  12361  fprodseq  12369  fprodf1o  12374  prodsnf  12378  fprodfac  12401  fprodabs  12402  ege2le3  12457  efaddlem  12460  eftlub  12476  tanval3ap  12500  tannegap  12514  cosmul  12531  cos01bnd  12544  demoivreALT  12560  flodddiv4  12722  dfgcd3  12806  absmulgcd  12813  nninfctlemfo  12836  sqpweven  12974  2sqpwodd  12975  crth  13025  eulerthlema  13031  phisum  13042  pythagtriplem14  13079  pythagtriplem19  13084  pcmul  13103  pcfac  13152  4sqlem12  13204  ballotfilemfp1  13283  ballotfilemsf1o  13309  ctiunctlemfo  13382  setsslnid  13456  qusgrp2  13969  mulgnngzsum  13983  mulgnn0gzsum  13984  mulgnn0p1  13989  mulgneg  13996  mulgnn0dir  14008  qusghm  14138  gzsumconst  14227  gzsummhm  14229  gzsumsplit0  14232  gsumvalfi  14236  gzsumgsum  14239  gsummptfidmadd  14245  srgpcomp  14378  opprrng  14466  opprring  14468  oppr1g  14472  invrfvald  14513  rdivmuldivd  14535  lmodvsmmulgdi  14744  lmodsubdi  14765  rmodislmodlem  14771  qusrhm  14949  quscrng  14954  mulgrhm  15028  asclmulg  15128  txbasval  15459  plymullem1  15940  rplogbchbase  16147  pellexlem2  16191  ppiqfl  16227  sgmmul  16251  chtublem  16256  bposlem9  16280  lgsdir2  16318  lgsdir  16320  lgsdi  16322  lgsdirnn0  16332  lgsdinn0  16333  lgsquad3  16369  vtxdgop  16699  qdiff  17265