Theorem 3eqtr2d 2216

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 2213	. 2 |- ( ph -> A = C )
4		3eqtr2d.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtrd 2210	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 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:  fmptapd  5707  rdgisucinc  6385  ctm  7107  mulidnq  7387  ltrnqg  7418  recexprlem1ssl  7631  recexprlem1ssu  7632  ltmprr  7640  mulcmpblnrlemg  7738  caucvgsrlemoffcau  7796  negsub  8204  neg2sub  8216  divmuleqap  8673  divneg2ap  8692  qapne  9638  seqvalcd  10458  binom2  10631  bcpasc  10745  crim  10866  remullem  10879  max0addsup  11227  summodclem2a  11388  isum1p  11499  geo2sum  11521  cvgratz  11539  efi4p  11724  tanaddap  11746  addcos  11753  cos2tsin  11758  demoivreALT  11780  omeo  11902  sqgcd  12029  eulerthlemth  12231  pythagtriplem16  12278  fldivp1  12345  pockthlem  12353  4sqlem10  12384  grpinvid2  12924  mulgaddcomlem  13004  mulgmodid  13020  ablsubsub  13119  ablsubsub4  13120  opprunitd  13277  txrest  13746  limccnpcntop  14114  dvrecap  14147  cosq34lt1  14241  lgseisenlem1  14420