Theorem 3eqtr2d 2214

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
3eqtr2d	|- ( ph -> A = D )

Proof of Theorem 3eqtr2d

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 |- ( ph -> A = B )
2		3eqtr2d.2	. . 3 |- ( ph -> C = B )
3	1, 2	eqtr4d 2211	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2208	1 |- ( ph -> A = D )

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  fmptapd  5699  rdgisucinc  6376  ctm  7098  mulidnq  7363  ltrnqg  7394  recexprlem1ssl  7607  recexprlem1ssu  7608  ltmprr  7616  mulcmpblnrlemg  7714  caucvgsrlemoffcau  7772  negsub  8179  neg2sub  8191  divmuleqap  8647  divneg2ap  8666  qapne  9612  seqvalcd  10429  binom2  10601  bcpasc  10714  crim  10835  remullem  10848  max0addsup  11196  summodclem2a  11357  isum1p  11468  geo2sum  11490  cvgratz  11508  efi4p  11693  tanaddap  11715  addcos  11722  cos2tsin  11727  demoivreALT  11749  omeo  11870  sqgcd  11997  eulerthlemth  12199  pythagtriplem16  12246  fldivp1  12313  pockthlem  12321  4sqlem10  12352  grpinvid2  12796  mulgaddcomlem  12875  mulgmodid  12891  ablsubsub  12929  ablsubsub4  12930  txrest  13356  limccnpcntop  13724  dvrecap  13757  cosq34lt1  13851