Theorem 3eqtr2rd 2803

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 2799	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2797	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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  nneob  8665  xp1d2m1eqxm1d2  12600  negmod  14059  modeqmodmin  14084  faclbnd2  14435  cats1un  14870  cjmulval  15312  fsumsplit  15907  fzosump1  15918  bcxmas  16004  trireciplem  16031  geo2sum  16042  geo2lim  16044  geoisum1c  16049  mertenslem1  16053  fprodsplit  16133  risefallfac  16191  bpolydiflem  16220  eftlub  16277  tanadd  16335  addsin  16338  subsin  16339  subcos  16343  sadadd2lem2  16620  qredeu  16833  zsqrtelqelz  16934  4sqlem15  17137  rcaninv  17969  resssetc  18267  resscatc  18284  curfcl  18406  mulgaddcomlem  19307  conjghm  19463  gasubg  19516  dfod2  19778  efginvrel2  19941  efgcpbllemb  19969  odadd2  20063  frgpnabllem1  20087  srgbinomlem3  20454  pws1  20554  prdslmodd  21244  znunithash  21870  frlmipval  22085  frlmlbs  22103  psrlmod  22267  matunitlindflem2  22995  restcld  23490  clmneg  25402  rrxds  25714  itg2monolem1  26071  itgconst  26139  dvexp  26273  dvfsumabs  26343  dvtaylp  26697  taylthlem2  26701  tangtx  26834  logsqrt  27032  zrtelqelz  27086  lawcoslem1  27143  chordthmlem2  27161  chordthmlem4  27163  tanatan  27247  atanbndlem  27253  amgmlem  27317  basellem3  27410  basellem5  27412  mpodvdsmulf1o  27521  dvdsmulf1o  27523  chtub  27539  fsumvma  27540  lgsquad2lem1  27711  2sqlem8  27753  dchrmusum2  27821  logsqvma  27869  pntrlog2bndlem4  27907  pw2divsnegd  28835  miriso  29142  lnssplnglem  29269  lmieu  29289  ttgcontlem1  29462  brbtwn2  29483  ax5seglem1  29506  axcontlem2  29543  axcontlem4  29545  clwwlkel  30637  vc0  31176  hvsubdistr2  31652  adjlnop  32688  adjcoi  32702  cnvbraval  32712  fpwrelmap  33325  fsumiunle  33420  xrge0adddir  33579  cycpm2tr  33680  cycpmco2lem4  33690  cycpmco2lem7  33693  cyc3genpmlem  33712  archirngz  33750  archiabllem1b  33753  erler  33826  qusrn  33960  ressply10g  34099  ply1gsumz  34131  selvply1rhm0  34158  vietalem  34211  fedgmullem1  34261  fedgmullem2  34262  dimlssid  34264  constrrtcc  34367  rspectopn  34499  xrge0pluscn  34572  esumfzf  34701  esumiun  34726  volmeas  34864  omssubadd  34932  breprexplemc  35261  bnj553  35528  cvmliftlem6  36055  cvmliftlem10  36059  cvmlift2lem3  36070  finxpreclem4  38317  sin2h  38533  poimirlem16  38554  heibor  38755  ghomdiv  38826  3atlem1  40540  atmod3i2  40922  trljat2  41224  cdleme1  41284  cdleme22eALTN  41402  cdlemh2  41873  dihglblem3N  42352  dih1dimatlem0  42385  djhlsmcl  42471  mapdpglem30  42759  hdmapneg  42903  hgmapval1  42950  hgmapmul  42952  sn-1ne2  43330  sn-addrid  43472  fltnltalem  43673  3cubeslem3r  43697  3cubeslem4  43699  proot1ex  44197  tfsconcatfv  44342  dirkerper  47105  fourierdlem49  47164  fourierdlem83  47198  fourierdlem92  47207  sigarperm  47869  sigaradd  47875  cos5t  47924  fmtnorec1  48621  lincresunit3lem2  49591  itsclc0yqsollem1  49873  itsclinecirc0b  49885  fuco11bALT  50445  prstchomval  50666  sinhpcosh  50832  amgmwlem  50986