Theorem 3eqtr2rd 2779

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr2d.2	⊢ (𝜑 → 𝐶 = 𝐵)
3eqtr2d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtr2rd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2775	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2773	1 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  nneob  8651  xp1d2m1eqxm1d2  12462  negmod  13877  modeqmodmin  13902  faclbnd2  14247  cats1un  14667  cjmulval  15088  fsumsplit  15683  fzosump1  15694  bcxmas  15777  trireciplem  15804  geo2sum  15815  geo2lim  15817  geoisum1c  15822  mertenslem1  15826  fprodsplit  15906  risefallfac  15964  bpolydiflem  15994  eftlub  16048  tanadd  16106  addsin  16109  subsin  16110  subcos  16114  sadadd2lem2  16387  qredeu  16591  zsqrtelqelz  16690  4sqlem15  16888  rcaninv  17737  resssetc  18038  resscatc  18055  estrreslem1OLD  18085  curfcl  18181  mulgaddcomlem  18971  conjghm  19117  gasubg  19160  dfod2  19426  efginvrel2  19589  efgcpbllemb  19617  odadd2  19711  frgpnabllem1  19735  srgbinomlem3  20044  pws1  20131  prdslmodd  20572  znunithash  21111  frlmipval  21325  frlmlbs  21343  psrlmod  21512  restcld  22667  clmneg  24588  rrxds  24901  itg2monolem1  25259  itgconst  25327  dvexp  25461  dvfsumabs  25531  dvtaylp  25873  taylthlem2  25877  tangtx  26006  logsqrt  26203  lawcoslem1  26309  chordthmlem2  26327  chordthmlem4  26329  tanatan  26413  atanbndlem  26419  amgmlem  26483  basellem3  26576  basellem5  26578  dvdsmulf1o  26687  chtub  26704  fsumvma  26705  lgsquad2lem1  26876  2sqlem8  26918  dchrmusum2  26986  logsqvma  27034  pntrlog2bndlem4  27072  miriso  27910  lmieu  28024  ttgcontlem1  28131  brbtwn2  28152  ax5seglem1  28175  axcontlem2  28212  axcontlem4  28214  clwwlkel  29288  vc0  29814  hvsubdistr2  30290  adjlnop  31326  adjcoi  31340  cnvbraval  31350  fpwrelmap  31945  fsumiunle  32022  xrge0adddir  32180  cycpm2tr  32265  cycpmco2lem4  32275  cycpmco2lem7  32278  cyc3genpmlem  32297  archirngz  32322  archiabllem1b  32325  qusrn  32508  ressply10g  32644  ply1gsumz  32657  fedgmullem1  32702  fedgmullem2  32703  rspectopn  32835  xrge0pluscn  32908  esumfzf  33055  esumiun  33080  volmeas  33217  omssubadd  33287  breprexplemc  33632  bnj553  33897  cvmliftlem6  34269  cvmliftlem10  34273  cvmlift2lem3  34284  finxpreclem4  36263  sin2h  36466  matunitlindflem2  36473  poimirlem16  36492  heibor  36677  ghomdiv  36748  3atlem1  38342  atmod3i2  38724  trljat2  39026  cdleme1  39086  cdleme22eALTN  39204  cdlemh2  39675  dihglblem3N  40154  dih1dimatlem0  40187  djhlsmcl  40273  mapdpglem30  40561  hdmapneg  40705  hgmapval1  40752  hgmapmul  40754  sn-1ne2  41176  zrtelqelz  41231  sn-addrid  41289  fltnltalem  41400  3cubeslem3r  41410  3cubeslem4  41412  proot1ex  41928  tfsconcatfv  42076  dirkerper  44798  fourierdlem83  44891  fourierdlem92  44900  sigarperm  45562  sigaradd  45568  fmtnorec1  46191  lincresunit3lem2  47114  itsclc0yqsollem1  47401  itsclinecirc0b  47413  prstchomval  47647  sinhpcosh  47738  amgmwlem  47802