Theorem 3eqtr2rd 2651

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  nneob  7619  xp1d2m1eqxm1d2  11163  negmod  12577  modeqmodmin  12602  faclbnd2  12940  cats1un  13327  cjmulval  13733  fsumsplit  14318  fzosump1  14325  bcxmas  14406  trireciplem  14433  geo2sum  14443  geo2lim  14445  geoisum1c  14450  mertenslem1  14455  fprodsplit  14535  risefallfac  14594  bpolydiflem  14624  eftlub  14678  tanadd  14736  addsin  14739  subsin  14740  subcos  14744  sadadd2lem2  15010  qredeu  15210  zsqrtelqelz  15304  4sqlem15  15501  rcaninv  16277  resssetc  16565  resscatc  16578  estrreslem1  16600  curfcl  16695  mulgaddcomlem  17386  conjghm  17514  gasubg  17558  dfod2  17804  efginvrel2  17963  efgcpbllemb  17991  odadd2  18075  frgpnabllem1  18099  srgbinomlem3  18365  pws1  18439  prdslmodd  18790  psrlmod  19222  znunithash  19732  frlmipval  19937  frlmlbs  19955  restcld  20786  clmneg  22689  rrxds  22989  itg2monolem1  23323  itgconst  23391  dvexp  23522  dvfsumabs  23590  dvtaylp  23928  taylthlem2  23932  tangtx  24061  logsqrt  24250  lawcoslem1  24345  chordthmlem2  24360  chordthmlem4  24362  tanatan  24446  atanbndlem  24452  amgmlem  24516  basellem3  24609  basellem5  24611  dvdsmulf1o  24720  chtub  24737  fsumvma  24738  lgsquad2lem1  24909  2sqlem8  24951  dchrmusum2  24983  logsqvma  25031  pntrlog2bndlem4  25069  miriso  25365  lmieu  25476  sacgr  25522  ttgcontlem1  25565  brbtwn2  25585  ax5seglem1  25608  axcontlem2  25645  axcontlem4  25647  vc0  26813  hvsubdistr2  27291  adjlnop  28329  adjcoi  28343  cnvbraval  28353  fpwrelmap  28896  xrge0adddir  29023  archirngz  29074  archiabllem1b  29077  xrge0pluscn  29314  esumfzf  29458  esumiun  29483  volmeas  29621  omssubadd  29689  bnj553  30222  cvmliftlem6  30526  cvmliftlem10  30530  cvmlift2lem3  30541  finxpreclem4  32407  sin2h  32569  matunitlindflem2  32576  poimirlem16  32595  heibor  32790  ghomdiv  32861  3atlem1  33787  atmod3i2  34169  trljat2  34472  cdleme1  34532  cdleme22eALTN  34651  cdlemh2  35122  dihglblem3N  35602  dih1dimatlem0  35635  djhlsmcl  35721  mapdpglem30  36009  hdmapneg  36156  hgmapval1  36203  hgmapmul  36205  proot1ex  36798  dirkerper  38989  fourierdlem83  39082  fourierdlem92  39091  sigarperm  39698  sigaradd  39704  fmtnorec1  39987  lincresunit3lem2  42063  sinhpcosh  42280  amgmwlem  42357