Theorem 3eqtr2rd 2210

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 2206	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2204	1 |- ( ph -> D = A )

Syntax hints:   -> wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  difinfsn  7073  nnnninfeq  7100  prarloclemlo  7443  recexgt0sr  7722  xp1d2m1eqxm1d2  9117  qnegmod  10312  modqeqmodmin  10337  faclbnd2  10663  cjmulval  10839  fsumsplit  11357  fzosump1  11367  isumclim3  11373  bcxmas  11439  trireciplem  11450  geo2sum  11464  geo2lim  11466  geoisum1c  11470  cvgratnnlemseq  11476  mertenslemi1  11485  fprodsplitdc  11546  eftlub  11640  addsin  11692  subsin  11693  subcos  11697  qredeu  12038  nn0sqrtelqelz  12147  strslfv2d  12445  dvexp  13390  tangtx  13474  logsqrt  13558  2sqlem8  13674