Theorem 3eqtr2rd 2228

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

Hypotheses

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

Assertion

Ref	Expression
3eqtr2rd	|- ( ph -> D = A )

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 |- ( ph -> A = B )
2		3eqtr2d.2	. . 3 |- ( ph -> C = B )
3	1, 2	eqtr4d 2224	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2222	1 |- ( ph -> D = A )

Syntax hints:   -> wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2170

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

This theorem is referenced by:  difinfsn  7116  nnnninfeq  7143  prarloclemlo  7510  recexgt0sr  7789  xp1d2m1eqxm1d2  9188  qnegmod  10386  modqeqmodmin  10411  faclbnd2  10739  cjmulval  10914  fsumsplit  11432  fzosump1  11442  isumclim3  11448  bcxmas  11514  trireciplem  11525  geo2sum  11539  geo2lim  11541  geoisum1c  11545  cvgratnnlemseq  11551  mertenslemi1  11560  fprodsplitdc  11621  eftlub  11715  addsin  11767  subsin  11768  subcos  11772  qredeu  12114  nn0sqrtelqelz  12223  strslfv2d  12522  mulgaddcomlem  13050  conjghm  13175  dvexp  14558  tangtx  14642  logsqrt  14726  2sqlem8  14853