Theorem 3eqtr3rd 2136

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

Syntax hints:   → wi 4   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

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

This theorem is referenced by:  fcofo  5601  fcof1o  5606  frecabcl  6202  nnaword  6310  enomnilem  6881  fodju0  6890  pn0sr  7414  negeu  7770  add20  8049  2halves  8743  bcnn  10280  bcpasc  10289  resqrexlemover  10558  fsumneg  10994  geolim  11054  geolim2  11055  mertensabs  11080  sincossq  11188  demoivre  11211  eirraplem  11213  gcdid  11404  phiprmpw  11625  ioo2bl  12319