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  4966  fvco4  5780  phplem4  7162  phplem4on  7175  omp1eomlem  7440  ctssdclemn0  7456  recexnq  7763  prarloclemcalc  7875  addcomprg  7951  mulcomprg  7953  mulcmpblnrlemg  8113  axmulass  8246  divnegap  9044  modqlt  10790  modqmulnn  10799  seq3val  10917  seqvalcd  10918  seq3caopr3  10948  seqcaopr3g  10949  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1o  10974  bcval5  11222  omgadd  11263  hashmap  11289  seq3coll  11315  s3s4d  11596  s2s5d  11597  s5s2d  11598  cjreb  11652  recj  11653  imcj  11661  imval2  11680  resqrexlemover  11797  sqrtmul  11822  amgm2  11906  maxabslemab  11994  xrmaxadd  12051  summodclem2a  12172  fsumf1o  12181  sumsnf  12200  sumsplitdc  12223  fsummulc2  12239  binom  12275  bcxmas  12280  expcnvap0  12293  expcnv  12295  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  prodmodclem3  12366  fprodseq  12374  fprodf1o  12379  prodsnf  12383  fprodfac  12406  fprodabs  12407  ege2le3  12462  efaddlem  12465  eftlub  12481  tanval3ap  12505  tannegap  12519  cosmul  12536  cos01bnd  12549  demoivreALT  12565  flodddiv4  12727  dfgcd3  12811  absmulgcd  12818  nninfctlemfo  12841  sqpweven  12979  2sqpwodd  12980  crth  13030  eulerthlema  13036  phisum  13047  pythagtriplem14  13084  pythagtriplem19  13089  pcmul  13108  pcfac  13157  4sqlem12  13209  ballotfilemfp1  13288  ballotfilemsf1o  13314  ctiunctlemfo  13387  setsslnid  13461  qusgrp2  13974  mulgnngzsum  13988  mulgnn0gzsum  13989  mulgnn0p1  13994  mulgneg  14001  mulgnn0dir  14013  qusghm  14143  gzsumconst  14232  gzsummhm  14234  gzsumsplit0  14237  gsumvalfi  14241  gzsumgsum  14244  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsumresfi  14262  srgpcomp  14400  opprrng  14490  opprring  14492  oppr1g  14496  invrfvald  14537  rdivmuldivd  14559  lmodvsmmulgdi  14768  lmodsubdi  14789  rmodislmodlem  14795  qusrhm  14973  quscrng  14978  mulgrhm  15052  asclmulg  15152  txbasval  15510  plymullem1  15991  rplogbchbase  16203  pellexlem2  16247  ppiqfl  16283  sgmmul  16307  chtublem  16312  bposlem9  16336  lgsdir2  16374  lgsdir  16376  lgsdi  16378  lgsdirnn0  16388  lgsdinn0  16389  lgsquad3  16425  vtxdgop  16755  qdiff  17322