Theorem 3eqtr2rd 2217

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  difinfsn  7098  nnnninfeq  7125  prarloclemlo  7492  recexgt0sr  7771  xp1d2m1eqxm1d2  9170  qnegmod  10368  modqeqmodmin  10393  faclbnd2  10721  cjmulval  10896  fsumsplit  11414  fzosump1  11424  isumclim3  11430  bcxmas  11496  trireciplem  11507  geo2sum  11521  geo2lim  11523  geoisum1c  11527  cvgratnnlemseq  11533  mertenslemi1  11542  fprodsplitdc  11603  eftlub  11697  addsin  11749  subsin  11750  subcos  11754  qredeu  12096  nn0sqrtelqelz  12205  strslfv2d  12504  mulgaddcomlem  13004  dvexp  14145  tangtx  14229  logsqrt  14313  2sqlem8  14440