Theorem 3eqtr4rd 2248

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  csbcnvg  4861  fvco4  5650  phplem4  6951  phplem4on  6963  omp1eomlem  7195  ctssdclemn0  7211  recexnq  7502  prarloclemcalc  7614  addcomprg  7690  mulcomprg  7692  mulcmpblnrlemg  7852  axmulass  7985  divnegap  8778  modqlt  10476  modqmulnn  10485  seq3val  10603  seqvalcd  10604  seq3caopr3  10634  seqcaopr3g  10635  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  seq3f1o  10660  bcval5  10906  omgadd  10945  seq3coll  10985  cjreb  11148  recj  11149  imcj  11157  imval2  11176  resqrexlemover  11292  sqrtmul  11317  amgm2  11400  maxabslemab  11488  xrmaxadd  11543  summodclem2a  11663  fsumf1o  11672  sumsnf  11691  sumsplitdc  11714  fsummulc2  11730  binom  11766  bcxmas  11771  expcnvap0  11784  expcnv  11786  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  prodmodclem3  11857  fprodseq  11865  fprodf1o  11870  prodsnf  11874  fprodfac  11897  fprodabs  11898  ege2le3  11953  efaddlem  11956  eftlub  11972  tanval3ap  11996  tannegap  12010  cosmul  12027  cos01bnd  12040  demoivreALT  12056  flodddiv4  12218  dfgcd3  12302  absmulgcd  12309  nninfctlemfo  12332  sqpweven  12468  2sqpwodd  12469  crth  12517  eulerthlema  12523  phisum  12534  pythagtriplem14  12571  pythagtriplem19  12576  pcmul  12595  pcfac  12644  4sqlem12  12696  ctiunctlemfo  12781  setsslnid  12855  qusgrp2  13420  mulgnngsum  13434  mulgnn0gsum  13435  mulgnn0p1  13440  mulgneg  13447  mulgnn0dir  13459  qusghm  13589  gsumfzconst  13648  gsumfzmhm  13650  srgpcomp  13723  opprrng  13810  opprring  13812  oppr1g  13815  invrfvald  13855  rdivmuldivd  13877  lmodvsmmulgdi  14056  lmodsubdi  14077  rmodislmodlem  14083  qusrhm  14261  quscrng  14266  mulgrhm  14342  txbasval  14710  plymullem1  15191  rplogbchbase  15393  sgmmul  15439  lgsdir2  15481  lgsdir  15483  lgsdi  15485  lgsdirnn0  15495  lgsdinn0  15496  lgsquad3  15532