Theorem 3eqtr2rd 2271

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  difinfsn  7359  nnnninfeq  7387  prarloclemlo  7774  recexgt0sr  8053  xp1d2m1eqxm1d2  9456  qnegmod  10694  modqeqmodmin  10719  faclbnd2  11067  cats1un  11368  cjmulval  11528  fsumsplit  12048  fzosump1  12058  isumclim3  12064  bcxmas  12130  trireciplem  12141  geo2sum  12155  geo2lim  12157  geoisum1c  12161  cvgratnnlemseq  12167  mertenslemi1  12176  fprodsplitdc  12237  eftlub  12331  addsin  12383  subsin  12384  subcos  12388  qredeu  12749  nn0sqrtelqelz  12858  4sqlem15  13058  strslfv2d  13205  mulgaddcomlem  13812  conjghm  13943  dvexp  15522  tangtx  15649  logsqrt  15734  mpodvdsmulf1o  15804  lgsquad2lem1  15900  2sqlem8  15942