Theorem 3eqtr2rd 2236

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  difinfsn  7166  nnnninfeq  7194  prarloclemlo  7561  recexgt0sr  7840  xp1d2m1eqxm1d2  9244  qnegmod  10461  modqeqmodmin  10486  faclbnd2  10834  cjmulval  11053  fsumsplit  11572  fzosump1  11582  isumclim3  11588  bcxmas  11654  trireciplem  11665  geo2sum  11679  geo2lim  11681  geoisum1c  11685  cvgratnnlemseq  11691  mertenslemi1  11700  fprodsplitdc  11761  eftlub  11855  addsin  11907  subsin  11908  subcos  11912  qredeu  12265  nn0sqrtelqelz  12374  4sqlem15  12574  strslfv2d  12721  mulgaddcomlem  13275  conjghm  13406  dvexp  14947  tangtx  15074  logsqrt  15159  mpodvdsmulf1o  15226  lgsquad2lem1  15322  2sqlem8  15364