Theorem 3eqtr3rd 2212

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  fcofo  5763  fcof1o  5768  frecabcl  6378  nnaword  6490  nninfisol  7109  enomnilem  7114  fodju0  7123  enmkvlem  7137  enwomnilem  7145  pn0sr  7733  negeu  8110  add20  8393  2halves  9107  bcnn  10691  bcpasc  10700  resqrexlemover  10974  fsumneg  11414  geolim  11474  geolim2  11475  mertensabs  11500  sincossq  11711  demoivre  11735  eirraplem  11739  gcdid  11941  gcdmultipled  11948  phiprmpw  12176  pythagtriplem12  12229  expnprm  12305  grpinvid1  12754  ioo2bl  13337  ptolemy  13539  coskpi  13563  logbgcd1irr  13679  logbgcd1irraplemap  13681