Theorem 3eqtr2rd 2247

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  difinfsn  7228  nnnninfeq  7256  prarloclemlo  7642  recexgt0sr  7921  xp1d2m1eqxm1d2  9325  qnegmod  10551  modqeqmodmin  10576  faclbnd2  10924  cats1un  11212  cjmulval  11314  fsumsplit  11833  fzosump1  11843  isumclim3  11849  bcxmas  11915  trireciplem  11926  geo2sum  11940  geo2lim  11942  geoisum1c  11946  cvgratnnlemseq  11952  mertenslemi1  11961  fprodsplitdc  12022  eftlub  12116  addsin  12168  subsin  12169  subcos  12173  qredeu  12534  nn0sqrtelqelz  12643  4sqlem15  12843  strslfv2d  12990  mulgaddcomlem  13596  conjghm  13727  dvexp  15298  tangtx  15425  logsqrt  15510  mpodvdsmulf1o  15577  lgsquad2lem1  15673  2sqlem8  15715