Theorem 3eqtr2rd 2245

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 2241	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2239	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  difinfsn  7202  nnnninfeq  7230  prarloclemlo  7607  recexgt0sr  7886  xp1d2m1eqxm1d2  9290  qnegmod  10514  modqeqmodmin  10539  faclbnd2  10887  cjmulval  11199  fsumsplit  11718  fzosump1  11728  isumclim3  11734  bcxmas  11800  trireciplem  11811  geo2sum  11825  geo2lim  11827  geoisum1c  11831  cvgratnnlemseq  11837  mertenslemi1  11846  fprodsplitdc  11907  eftlub  12001  addsin  12053  subsin  12054  subcos  12058  qredeu  12419  nn0sqrtelqelz  12528  4sqlem15  12728  strslfv2d  12875  mulgaddcomlem  13481  conjghm  13612  dvexp  15183  tangtx  15310  logsqrt  15395  mpodvdsmulf1o  15462  lgsquad2lem1  15558  2sqlem8  15600