Theorem 3eqtr4rd 2273

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbcnvg  4906  fvco4  5708  phplem4  7024  phplem4on  7037  omp1eomlem  7272  ctssdclemn0  7288  recexnq  7588  prarloclemcalc  7700  addcomprg  7776  mulcomprg  7778  mulcmpblnrlemg  7938  axmulass  8071  divnegap  8864  modqlt  10567  modqmulnn  10576  seq3val  10694  seqvalcd  10695  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1o  10751  bcval5  10997  omgadd  11036  seq3coll  11077  cjreb  11392  recj  11393  imcj  11401  imval2  11420  resqrexlemover  11536  sqrtmul  11561  amgm2  11644  maxabslemab  11732  xrmaxadd  11787  summodclem2a  11907  fsumf1o  11916  sumsnf  11935  sumsplitdc  11958  fsummulc2  11974  binom  12010  bcxmas  12015  expcnvap0  12028  expcnv  12030  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  prodmodclem3  12101  fprodseq  12109  fprodf1o  12114  prodsnf  12118  fprodfac  12141  fprodabs  12142  ege2le3  12197  efaddlem  12200  eftlub  12216  tanval3ap  12240  tannegap  12254  cosmul  12271  cos01bnd  12284  demoivreALT  12300  flodddiv4  12462  dfgcd3  12546  absmulgcd  12553  nninfctlemfo  12576  sqpweven  12712  2sqpwodd  12713  crth  12761  eulerthlema  12767  phisum  12778  pythagtriplem14  12815  pythagtriplem19  12820  pcmul  12839  pcfac  12888  4sqlem12  12940  ctiunctlemfo  13025  setsslnid  13099  qusgrp2  13665  mulgnngsum  13679  mulgnn0gsum  13680  mulgnn0p1  13685  mulgneg  13692  mulgnn0dir  13704  qusghm  13834  gsumfzconst  13893  gsumfzmhm  13895  srgpcomp  13968  opprrng  14055  opprring  14057  oppr1g  14060  invrfvald  14101  rdivmuldivd  14123  lmodvsmmulgdi  14302  lmodsubdi  14323  rmodislmodlem  14329  qusrhm  14507  quscrng  14512  mulgrhm  14588  txbasval  14956  plymullem1  15437  rplogbchbase  15639  sgmmul  15685  lgsdir2  15727  lgsdir  15729  lgsdi  15731  lgsdirnn0  15741  lgsdinn0  15742  lgsquad3  15778  vtxdgop  16051