Theorem 3eqtr2rd 2278

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  difinfsn  7440  nnnninfeq  7468  prarloclemlo  7861  recexgt0sr  8140  xp1d2m1eqxm1d2  9562  qnegmod  10819  modqeqmodmin  10844  faclbnd2  11194  cats1un  11507  cjmulval  11667  sq01  11674  fsumsplit  12190  fzosump1  12200  isumclim3  12206  bcxmas  12272  trireciplem  12283  geo2sum  12297  geo2lim  12299  geoisum1c  12303  cvgratnnlemseq  12309  mertenslemi1  12318  fprodsplitdc  12379  eftlub  12473  addsin  12525  subsin  12526  subcos  12530  qredeu  12891  nn0sqrtelqelz  13002  4sqlem15  13204  strslfv2d  13444  mulgaddcomlem  13997  conjghm  14128  dvexp  15861  tangtx  15989  logsqrt  16078  mpodvdsmulf1o  16185  lgsquad2lem1  16298  2sqlem8  16340