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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  difinfsn  7430  nnnninfeq  7458  prarloclemlo  7851  recexgt0sr  8130  xp1d2m1eqxm1d2  9537  qnegmod  10784  modqeqmodmin  10809  faclbnd2  11158  cats1un  11471  cjmulval  11631  sq01  11638  fsumsplit  12152  fzosump1  12162  isumclim3  12168  bcxmas  12234  trireciplem  12245  geo2sum  12259  geo2lim  12261  geoisum1c  12265  cvgratnnlemseq  12271  mertenslemi1  12280  fprodsplitdc  12341  eftlub  12435  addsin  12487  subsin  12488  subcos  12492  qredeu  12853  nn0sqrtelqelz  12962  4sqlem15  13162  strslfv2d  13373  mulgaddcomlem  13925  conjghm  14056  dvexp  15735  tangtx  15862  logsqrt  15948  mpodvdsmulf1o  16018  lgsquad2lem1  16114  2sqlem8  16156