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  5710  rdgisucinc  6389  ctm  7111  mulidnq  7391  ltrnqg  7422  recexprlem1ssl  7635  recexprlem1ssu  7636  ltmprr  7644  mulcmpblnrlemg  7742  caucvgsrlemoffcau  7800  negsub  8208  neg2sub  8220  divmuleqap  8677  divneg2ap  8696  qapne  9642  seqvalcd  10462  binom2  10635  bcpasc  10749  crim  10870  remullem  10883  max0addsup  11231  summodclem2a  11392  isum1p  11503  geo2sum  11525  cvgratz  11543  efi4p  11728  tanaddap  11750  addcos  11757  cos2tsin  11762  demoivreALT  11784  omeo  11906  sqgcd  12033  eulerthlemth  12235  pythagtriplem16  12282  fldivp1  12349  pockthlem  12357  4sqlem10  12388  grpinvid2  12931  mulgaddcomlem  13012  mulgmodid  13028  ablsubsub  13127  ablsubsub4  13128  opprunitd  13285  lmodfopne  13422  txrest  13916  limccnpcntop  14284  dvrecap  14317  cosq34lt1  14411  lgseisenlem1  14590