Theorem 3eqtr2rd 2805

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  nneob  8703  xp1d2m1eqxm1d2  12640  negmod  14099  modeqmodmin  14124  faclbnd2  14476  cats1un  14912  cjmulval  15355  fsumsplit  15951  fzosump1  15962  bcxmas  16048  trireciplem  16075  geo2sum  16086  geo2lim  16088  geoisum1c  16093  mertenslem1  16097  fprodsplit  16177  risefallfac  16235  bpolydiflem  16264  eftlub  16321  tanadd  16379  addsin  16382  subsin  16383  subcos  16387  sadadd2lem2  16664  qredeu  16877  zsqrtelqelz  16978  4sqlem15  17181  rcaninv  18019  resssetc  18317  resscatc  18334  curfcl  18456  mulgaddcomlem  19357  conjghm  19513  gasubg  19567  dfod2  19829  efginvrel2  19992  efgcpbllemb  20020  odadd2  20114  frgpnabllem1  20138  srgbinomlem3  20505  pws1  20605  prdslmodd  21295  znunithash  21925  frlmipval  22140  frlmlbs  22158  psrlmod  22322  matunitlindflem2  23050  restcld  23545  clmneg  25457  rrxds  25769  itg2monolem1  26126  itgconst  26194  dvexp  26328  dvfsumabs  26398  dvtaylp  26754  taylthlem2  26758  tangtx  26891  logsqrt  27089  zrtelqelz  27143  lawcoslem1  27200  chordthmlem2  27218  chordthmlem4  27220  tanatan  27304  atanbndlem  27310  amgmlem  27374  basellem3  27467  basellem5  27469  mpodvdsmulf1o  27578  dvdsmulf1o  27580  chtub  27596  fsumvma  27597  lgsquad2lem1  27768  2sqlem8  27810  dchrmusum2  27878  logsqvma  27926  pntrlog2bndlem4  27964  pw2divsnegd  28892  miriso  29199  lnssplnglem  29326  lmieu  29346  ttgcontlem1  29519  brbtwn2  29540  ax5seglem1  29563  axcontlem2  29600  axcontlem4  29602  clwwlkel  30694  vc0  31233  hvsubdistr2  31709  adjlnop  32745  adjcoi  32759  cnvbraval  32769  fpwrelmap  33421  fsumiunle  33516  xrge0adddir  33678  cycpm2tr  33779  cycpmco2lem4  33789  cycpmco2lem7  33792  cyc3genpmlem  33811  archirngz  33849  archiabllem1b  33852  erler  33925  qusrn  34064  ressply10g  34202  ply1gsumz  34234  rngunsnply1chr2lem2  34251  selvply1rhm0  34269  vietalem  34322  fedgmullem1  34372  fedgmullem2  34373  dimlssid  34375  constrrtcc  34478  rspectopn  34610  xrge0pluscn  34683  esumfzf  34812  esumiun  34837  volmeas  34975  omssubadd  35043  breprexplemc  35372  bnj553  35639  cvmliftlem6  36263  cvmliftlem10  36267  cvmlift2lem3  36278  finxpreclem4  38585  sin2h  38801  poimirlem16  38822  heibor  39021  ghomdiv  39092  3atlem1  40806  atmod3i2  41188  trljat2  41490  cdleme1  41550  cdleme22eALTN  41668  cdlemh2  42139  dihglblem3N  42618  dih1dimatlem0  42651  djhlsmcl  42737  mapdpglem30  43025  hdmapneg  43169  hgmapval1  43216  hgmapmul  43218  sn-1ne2  43596  sn-addrid  43738  fltnltalem  43939  3cubeslem3r  43963  3cubeslem4  43965  proot1ex  44459  tfsconcatfv  44604  dirkerper  47379  fourierdlem49  47438  fourierdlem83  47472  fourierdlem92  47481  sigarperm  48143  sigaradd  48149  cos5t  48198  fmtnorec1  48895  lincresunit3lem2  49923  itsclc0yqsollem1  50205  itsclinecirc0b  50217  fuco11bALT  50791  prstchomval  51028  sinhpcosh  51238  amgmwlem  51415