Theorem 3eqtr3rd 2246

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

Syntax hints:   -> wi 4   = wceq 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197

This theorem is referenced by:  fcofo  5852  fcof1o  5857  frecabcl  6484  nnaword  6596  nninfisol  7234  enomnilem  7239  fodju0  7248  enmkvlem  7262  enwomnilem  7270  pn0sr  7883  negeu  8262  add20  8546  2halves  9265  bcnn  10900  bcpasc  10909  resqrexlemover  11292  fsumneg  11733  geolim  11793  geolim2  11794  mertensabs  11819  sincossq  12030  demoivre  12055  eirraplem  12059  gcdid  12278  gcdmultipled  12285  phiprmpw  12515  pythagtriplem12  12569  expnprm  12647  imasbas  13110  imasplusg  13111  imasmulr  13112  grpinvid1  13355  grpnpcan  13395  grplactcnv  13405  ghmgrp  13425  conjghm  13583  ringnegl  13784  ringnegr  13785  ringmneg2  13787  ring1  13792  rdivmuldivd  13877  lmodfopne  14059  lmodvsneg  14064  ioo2bl  14994  ptolemy  15267  coskpi  15291  logbgcd1irr  15410  logbgcd1irraplemap  15412  lgseisenlem3  15520  lgseisenlem4  15521  lgsquadlem1  15525  lgsquadlem2  15526