Theorem 3eqtr3rd 2207

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
2		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtr3d 2200	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2200	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  fcofo  5751  fcof1o  5756  frecabcl  6363  nnaword  6475  nninfisol  7093  enomnilem  7098  fodju0  7107  enmkvlem  7121  enwomnilem  7129  pn0sr  7708  negeu  8085  add20  8368  2halves  9082  bcnn  10666  bcpasc  10675  resqrexlemover  10948  fsumneg  11388  geolim  11448  geolim2  11449  mertensabs  11474  sincossq  11685  demoivre  11709  eirraplem  11713  gcdid  11915  gcdmultipled  11922  phiprmpw  12150  pythagtriplem12  12203  expnprm  12279  ioo2bl  13143  ptolemy  13345  coskpi  13369  logbgcd1irr  13485  logbgcd1irraplemap  13487