Theorem 3eqtr3rd 2249

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  fcofo  5876  fcof1o  5881  frecabcl  6508  nnaword  6620  nninfisol  7261  enomnilem  7266  fodju0  7275  enmkvlem  7289  enwomnilem  7297  pn0sr  7919  negeu  8298  add20  8582  2halves  9301  bcnn  10939  bcpasc  10948  wrdeqs1cat  11211  resqrexlemover  11436  fsumneg  11877  geolim  11937  geolim2  11938  mertensabs  11963  sincossq  12174  demoivre  12199  eirraplem  12203  gcdid  12422  gcdmultipled  12429  phiprmpw  12659  pythagtriplem12  12713  expnprm  12791  imasbas  13254  imasplusg  13255  imasmulr  13256  grpinvid1  13499  grpnpcan  13539  grplactcnv  13549  ghmgrp  13569  conjghm  13727  ringnegl  13928  ringnegr  13929  ringmneg2  13931  ring1  13936  rdivmuldivd  14021  lmodfopne  14203  lmodvsneg  14208  ioo2bl  15138  ptolemy  15411  coskpi  15435  logbgcd1irr  15554  logbgcd1irraplemap  15556  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem2  15670