Theorem 3eqtr2rd 2274

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  difinfsn  7404  nnnninfeq  7432  prarloclemlo  7825  recexgt0sr  8104  xp1d2m1eqxm1d2  9511  qnegmod  10758  modqeqmodmin  10783  faclbnd2  11132  cats1un  11441  cjmulval  11601  fsumsplit  12121  fzosump1  12131  isumclim3  12137  bcxmas  12203  trireciplem  12214  geo2sum  12228  geo2lim  12230  geoisum1c  12234  cvgratnnlemseq  12240  mertenslemi1  12249  fprodsplitdc  12310  eftlub  12404  addsin  12456  subsin  12457  subcos  12461  qredeu  12822  nn0sqrtelqelz  12931  4sqlem15  13131  strslfv2d  13342  mulgaddcomlem  13901  conjghm  14032  dvexp  15705  tangtx  15832  logsqrt  15917  mpodvdsmulf1o  15987  lgsquad2lem1  16083  2sqlem8  16125