Theorem 3eqtr2rd 2269

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  difinfsn  7278  nnnninfeq  7306  prarloclemlo  7692  recexgt0sr  7971  xp1d2m1eqxm1d2  9375  qnegmod  10603  modqeqmodmin  10628  faclbnd2  10976  cats1un  11269  cjmulval  11415  fsumsplit  11934  fzosump1  11944  isumclim3  11950  bcxmas  12016  trireciplem  12027  geo2sum  12041  geo2lim  12043  geoisum1c  12047  cvgratnnlemseq  12053  mertenslemi1  12062  fprodsplitdc  12123  eftlub  12217  addsin  12269  subsin  12270  subcos  12274  qredeu  12635  nn0sqrtelqelz  12744  4sqlem15  12944  strslfv2d  13091  mulgaddcomlem  13698  conjghm  13829  dvexp  15401  tangtx  15528  logsqrt  15613  mpodvdsmulf1o  15680  lgsquad2lem1  15776  2sqlem8  15818