Theorem 3eqtr3rd 2179

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

Hypotheses

Ref	Expression
3eqtr3d.1	|- ( ph -> A = B )
3eqtr3d.2	|- ( ph -> A = C )
3eqtr3d.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3eqtr3rd	|- ( ph -> D = C )

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 |- ( ph -> B = D )
2		3eqtr3d.1	. . 3 |- ( ph -> A = B )
3		3eqtr3d.2	. . 3 |- ( ph -> A = C )
4	2, 3	eqtr3d 2172	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2172	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  fcofo  5678  fcof1o  5683  frecabcl  6289  nnaword  6400  enomnilem  7003  fodju0  7012  pn0sr  7572  negeu  7946  add20  8229  2halves  8942  bcnn  10496  bcpasc  10505  resqrexlemover  10775  fsumneg  11213  geolim  11273  geolim2  11274  mertensabs  11299  sincossq  11444  demoivre  11468  eirraplem  11472  gcdid  11663  gcdmultipled  11670  phiprmpw  11887  ioo2bl  12701  ptolemy  12894  coskpi  12918