Theorem 3eqtr2rd 2776

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 2772	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2770	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  nneob  8582  xp1d2m1eqxm1d2  12393  negmod  13837  modeqmodmin  13862  faclbnd2  14212  cats1un  14642  cjmulval  15066  fsumsplit  15662  fzosump1  15673  bcxmas  15756  trireciplem  15783  geo2sum  15794  geo2lim  15796  geoisum1c  15801  mertenslem1  15805  fprodsplit  15887  risefallfac  15945  bpolydiflem  15975  eftlub  16032  tanadd  16090  addsin  16093  subsin  16094  subcos  16098  sadadd2lem2  16375  qredeu  16583  zsqrtelqelz  16683  4sqlem15  16885  rcaninv  17716  resssetc  18014  resscatc  18031  curfcl  18153  mulgaddcomlem  19025  conjghm  19176  gasubg  19229  dfod2  19491  efginvrel2  19654  efgcpbllemb  19682  odadd2  19776  frgpnabllem1  19800  srgbinomlem3  20161  pws1  20258  prdslmodd  20918  znunithash  21517  frlmipval  21732  frlmlbs  21750  psrlmod  21913  restcld  23114  clmneg  25035  rrxds  25347  itg2monolem1  25705  itgconst  25774  dvexp  25911  dvfsumabs  25983  dvtaylp  26332  taylthlem2  26336  taylthlem2OLD  26337  tangtx  26468  logsqrt  26667  zrtelqelz  26722  lawcoslem1  26779  chordthmlem2  26797  chordthmlem4  26799  tanatan  26883  atanbndlem  26889  amgmlem  26954  basellem3  27047  basellem5  27049  mpodvdsmulf1o  27158  dvdsmulf1o  27160  chtub  27177  fsumvma  27178  lgsquad2lem1  27349  2sqlem8  27391  dchrmusum2  27459  logsqvma  27507  pntrlog2bndlem4  27545  pw2divsnegd  28407  miriso  28691  lmieu  28805  ttgcontlem1  28906  brbtwn2  28927  ax5seglem1  28950  axcontlem2  28987  axcontlem4  28989  clwwlkel  30070  vc0  30598  hvsubdistr2  31074  adjlnop  32110  adjcoi  32124  cnvbraval  32134  fpwrelmap  32761  fsumiunle  32859  xrge0adddir  33049  cycpm2tr  33150  cycpmco2lem4  33160  cycpmco2lem7  33163  cyc3genpmlem  33182  archirngz  33220  archiabllem1b  33223  erler  33296  qusrn  33439  ressply10g  33597  ply1gsumz  33629  vietalem  33684  fedgmullem1  33735  fedgmullem2  33736  dimlssid  33738  constrrtcc  33841  rspectopn  33973  xrge0pluscn  34046  esumfzf  34175  esumiun  34200  volmeas  34337  omssubadd  34406  breprexplemc  34738  bnj553  35003  cvmliftlem6  35433  cvmliftlem10  35437  cvmlift2lem3  35448  finxpreclem4  37538  sin2h  37750  matunitlindflem2  37757  poimirlem16  37776  heibor  37961  ghomdiv  38032  3atlem1  39682  atmod3i2  40064  trljat2  40366  cdleme1  40426  cdleme22eALTN  40544  cdlemh2  41015  dihglblem3N  41494  dih1dimatlem0  41527  djhlsmcl  41613  mapdpglem30  41901  hdmapneg  42045  hgmapval1  42092  hgmapmul  42094  sn-1ne2  42462  sn-addrid  42618  fltnltalem  42847  3cubeslem3r  42871  3cubeslem4  42873  proot1ex  43380  tfsconcatfv  43525  dirkerper  46282  fourierdlem83  46375  fourierdlem92  46384  sigarperm  47046  sigaradd  47052  fmtnorec1  47725  lincresunit3lem2  48668  itsclc0yqsollem1  48950  itsclinecirc0b  48962  fuco11bALT  49525  prstchomval  49746  sinhpcosh  49927  amgmwlem  49989