Theorem 3eqtr3rd 2182

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 2175	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2175	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  fcofo  5693  fcof1o  5698  frecabcl  6304  nnaword  6415  enomnilem  7018  fodju0  7027  enmkvlem  7043  enwomnilem  7050  pn0sr  7603  negeu  7977  add20  8260  2halves  8973  bcnn  10535  bcpasc  10544  resqrexlemover  10814  fsumneg  11252  geolim  11312  geolim2  11313  mertensabs  11338  sincossq  11491  demoivre  11515  eirraplem  11519  gcdid  11710  gcdmultipled  11717  phiprmpw  11934  ioo2bl  12751  ptolemy  12953  coskpi  12977  logbgcd1irr  13092  logbgcd1irraplemap  13094