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  7204  nnnninfeq  7232  prarloclemlo  7609  recexgt0sr  7888  xp1d2m1eqxm1d2  9292  qnegmod  10516  modqeqmodmin  10541  faclbnd2  10889  cjmulval  11232  fsumsplit  11751  fzosump1  11761  isumclim3  11767  bcxmas  11833  trireciplem  11844  geo2sum  11858  geo2lim  11860  geoisum1c  11864  cvgratnnlemseq  11870  mertenslemi1  11879  fprodsplitdc  11940  eftlub  12034  addsin  12086  subsin  12087  subcos  12091  qredeu  12452  nn0sqrtelqelz  12561  4sqlem15  12761  strslfv2d  12908  mulgaddcomlem  13514  conjghm  13645  dvexp  15216  tangtx  15343  logsqrt  15428  mpodvdsmulf1o  15495  lgsquad2lem1  15591  2sqlem8  15633