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 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  nneob  8638  xp1d2m1eqxm1d2  12493  negmod  13948  modeqmodmin  13973  faclbnd2  14323  cats1un  14754  cjmulval  15192  fsumsplit  15788  fzosump1  15799  bcxmas  15885  trireciplem  15912  geo2sum  15923  geo2lim  15925  geoisum1c  15930  mertenslem1  15934  fprodsplit  16016  risefallfac  16074  bpolydiflem  16103  eftlub  16160  tanadd  16218  addsin  16221  subsin  16222  subcos  16226  sadadd2lem2  16503  qredeu  16711  zsqrtelqelz  16812  4sqlem15  17014  rcaninv  17846  resssetc  18144  resscatc  18161  curfcl  18283  mulgaddcomlem  19158  conjghm  19314  gasubg  19367  dfod2  19629  efginvrel2  19792  efgcpbllemb  19820  odadd2  19914  frgpnabllem1  19938  srgbinomlem3  20305  pws1  20402  prdslmodd  21090  znunithash  21714  frlmipval  21929  frlmlbs  21947  psrlmod  22109  restcld  23329  clmneg  25240  rrxds  25552  itg2monolem1  25909  itgconst  25978  dvexp  26112  dvfsumabs  26182  dvtaylp  26533  taylthlem2  26537  tangtx  26670  logsqrt  26869  zrtelqelz  26923  lawcoslem1  26980  chordthmlem2  26998  chordthmlem4  27000  tanatan  27084  atanbndlem  27090  amgmlem  27154  basellem3  27247  basellem5  27249  mpodvdsmulf1o  27358  dvdsmulf1o  27360  chtub  27376  fsumvma  27377  lgsquad2lem1  27548  2sqlem8  27590  dchrmusum2  27658  logsqvma  27706  pntrlog2bndlem4  27744  pw2divsnegd  28642  miriso  28947  lnssplnglem  29073  lmieu  29093  ttgcontlem1  29234  brbtwn2  29255  ax5seglem1  29278  axcontlem2  29315  axcontlem4  29317  clwwlkel  30397  vc0  30926  hvsubdistr2  31402  adjlnop  32438  adjcoi  32452  cnvbraval  32462  fpwrelmap  33078  fsumiunle  33173  xrge0adddir  33338  cycpm2tr  33439  cycpmco2lem4  33449  cycpmco2lem7  33452  cyc3genpmlem  33471  archirngz  33509  archiabllem1b  33512  erler  33585  qusrn  33718  ressply10g  33857  ply1gsumz  33889  selvply1rhm0  33916  vietalem  33969  fedgmullem1  34019  fedgmullem2  34020  dimlssid  34022  constrrtcc  34125  rspectopn  34257  xrge0pluscn  34330  esumfzf  34459  esumiun  34484  volmeas  34621  omssubadd  34690  breprexplemc  35019  bnj553  35286  cvmliftlem6  35782  cvmliftlem10  35786  cvmlift2lem3  35797  finxpreclem4  38060  sin2h  38281  matunitlindflem2  38288  poimirlem16  38307  heibor  38492  ghomdiv  38563  3atlem1  40277  atmod3i2  40659  trljat2  40961  cdleme1  41021  cdleme22eALTN  41139  cdlemh2  41610  dihglblem3N  42089  dih1dimatlem0  42122  djhlsmcl  42208  mapdpglem30  42496  hdmapneg  42640  hgmapval1  42687  hgmapmul  42689  sn-1ne2  43052  sn-addrid  43202  fltnltalem  43414  3cubeslem3r  43438  3cubeslem4  43440  proot1ex  43943  tfsconcatfv  44088  dirkerper  46830  fourierdlem49  46889  fourierdlem83  46923  fourierdlem92  46932  sigarperm  47594  sigaradd  47600  cos5t  47636  fmtnorec1  48309  lincresunit3lem2  49280  itsclc0yqsollem1  49562  itsclinecirc0b  49574  fuco11bALT  50136  prstchomval  50357  sinhpcosh  50538  amgmwlem  50669