Theorem 3eqtr4rd 2275

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

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

This theorem is referenced by:  csbcnvg  4920  fvco4  5727  phplem4  7084  phplem4on  7097  omp1eomlem  7336  ctssdclemn0  7352  recexnq  7653  prarloclemcalc  7765  addcomprg  7841  mulcomprg  7843  mulcmpblnrlemg  8003  axmulass  8136  divnegap  8928  modqlt  10641  modqmulnn  10650  seq3val  10768  seqvalcd  10769  seq3caopr3  10799  seqcaopr3g  10800  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seq3f1o  10825  bcval5  11071  omgadd  11111  seq3coll  11152  s3s4d  11433  s2s5d  11434  s5s2d  11435  cjreb  11489  recj  11490  imcj  11498  imval2  11517  resqrexlemover  11633  sqrtmul  11658  amgm2  11741  maxabslemab  11829  xrmaxadd  11884  summodclem2a  12005  fsumf1o  12014  sumsnf  12033  sumsplitdc  12056  fsummulc2  12072  binom  12108  bcxmas  12113  expcnvap0  12126  expcnv  12128  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  prodmodclem3  12199  fprodseq  12207  fprodf1o  12212  prodsnf  12216  fprodfac  12239  fprodabs  12240  ege2le3  12295  efaddlem  12298  eftlub  12314  tanval3ap  12338  tannegap  12352  cosmul  12369  cos01bnd  12382  demoivreALT  12398  flodddiv4  12560  dfgcd3  12644  absmulgcd  12651  nninfctlemfo  12674  sqpweven  12810  2sqpwodd  12811  crth  12859  eulerthlema  12865  phisum  12876  pythagtriplem14  12913  pythagtriplem19  12918  pcmul  12937  pcfac  12986  4sqlem12  13038  ctiunctlemfo  13123  setsslnid  13197  qusgrp2  13763  mulgnngsum  13777  mulgnn0gsum  13778  mulgnn0p1  13783  mulgneg  13790  mulgnn0dir  13802  qusghm  13932  gsumfzconst  13991  gsumfzmhm  13993  gsumsplit0  13996  srgpcomp  14067  opprrng  14154  opprring  14156  oppr1g  14159  invrfvald  14200  rdivmuldivd  14222  lmodvsmmulgdi  14402  lmodsubdi  14423  rmodislmodlem  14429  qusrhm  14607  quscrng  14612  mulgrhm  14688  txbasval  15061  plymullem1  15542  rplogbchbase  15744  pellexlem2  15775  sgmmul  15793  lgsdir2  15835  lgsdir  15837  lgsdi  15839  lgsdirnn0  15849  lgsdinn0  15850  lgsquad3  15886  vtxdgop  16216  qdiff  16764  gfsumval  16792  gsumgfsum  16796