Theorem 3eqtr2rd 2179

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  difinfsn  6985  prarloclemlo  7302  recexgt0sr  7581  xp1d2m1eqxm1d2  8972  qnegmod  10142  modqeqmodmin  10167  faclbnd2  10488  cjmulval  10660  fsumsplit  11176  fzosump1  11186  isumclim3  11192  bcxmas  11258  trireciplem  11269  geo2sum  11283  geo2lim  11285  geoisum1c  11289  cvgratnnlemseq  11295  mertenslemi1  11304  eftlub  11396  addsin  11449  subsin  11450  subcos  11454  qredeu  11778  nn0sqrtelqelz  11884  strslfv2d  12001  dvexp  12844  tangtx  12919  nninfalllemn  13202