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  4905  fvco4  5705  phplem4  7012  phplem4on  7025  omp1eomlem  7257  ctssdclemn0  7273  recexnq  7573  prarloclemcalc  7685  addcomprg  7761  mulcomprg  7763  mulcmpblnrlemg  7923  axmulass  8056  divnegap  8849  modqlt  10550  modqmulnn  10559  seq3val  10677  seqvalcd  10678  seq3caopr3  10708  seqcaopr3g  10709  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seq3f1o  10734  bcval5  10980  omgadd  11019  seq3coll  11059  cjreb  11372  recj  11373  imcj  11381  imval2  11400  resqrexlemover  11516  sqrtmul  11541  amgm2  11624  maxabslemab  11712  xrmaxadd  11767  summodclem2a  11887  fsumf1o  11896  sumsnf  11915  sumsplitdc  11938  fsummulc2  11954  binom  11990  bcxmas  11995  expcnvap0  12008  expcnv  12010  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  prodmodclem3  12081  fprodseq  12089  fprodf1o  12094  prodsnf  12098  fprodfac  12121  fprodabs  12122  ege2le3  12177  efaddlem  12180  eftlub  12196  tanval3ap  12220  tannegap  12234  cosmul  12251  cos01bnd  12264  demoivreALT  12280  flodddiv4  12442  dfgcd3  12526  absmulgcd  12533  nninfctlemfo  12556  sqpweven  12692  2sqpwodd  12693  crth  12741  eulerthlema  12747  phisum  12758  pythagtriplem14  12795  pythagtriplem19  12800  pcmul  12819  pcfac  12868  4sqlem12  12920  ctiunctlemfo  13005  setsslnid  13079  qusgrp2  13645  mulgnngsum  13659  mulgnn0gsum  13660  mulgnn0p1  13665  mulgneg  13672  mulgnn0dir  13684  qusghm  13814  gsumfzconst  13873  gsumfzmhm  13875  srgpcomp  13948  opprrng  14035  opprring  14037  oppr1g  14040  invrfvald  14080  rdivmuldivd  14102  lmodvsmmulgdi  14281  lmodsubdi  14302  rmodislmodlem  14308  qusrhm  14486  quscrng  14491  mulgrhm  14567  txbasval  14935  plymullem1  15416  rplogbchbase  15618  sgmmul  15664  lgsdir2  15706  lgsdir  15708  lgsdi  15710  lgsdirnn0  15720  lgsdinn0  15721  lgsquad3  15757