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  7267  nnnninfeq  7295  prarloclemlo  7681  recexgt0sr  7960  xp1d2m1eqxm1d2  9364  qnegmod  10591  modqeqmodmin  10616  faclbnd2  10964  cats1un  11253  cjmulval  11399  fsumsplit  11918  fzosump1  11928  isumclim3  11934  bcxmas  12000  trireciplem  12011  geo2sum  12025  geo2lim  12027  geoisum1c  12031  cvgratnnlemseq  12037  mertenslemi1  12046  fprodsplitdc  12107  eftlub  12201  addsin  12253  subsin  12254  subcos  12258  qredeu  12619  nn0sqrtelqelz  12728  4sqlem15  12928  strslfv2d  13075  mulgaddcomlem  13682  conjghm  13813  dvexp  15385  tangtx  15512  logsqrt  15597  mpodvdsmulf1o  15664  lgsquad2lem1  15760  2sqlem8  15802