Theorem 3eqtr3rd 2129

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 2122	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2122	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  fcofo  5563  fcof1o  5568  frecabcl  6164  nnaword  6268  enomnilem  6792  fodjuomnilem0  6800  pn0sr  7315  negeu  7671  add20  7950  2halves  8643  bcnn  10161  bcpasc  10170  resqrexlemover  10439  fsumneg  10841  geolim  10901  geolim2  10902  mertensabs  10927  sincossq  11035  demoivre  11058  eirraplem  11060  gcdid  11251  phiprmpw  11472