Theorem 3eqtr2d 2119

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

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  fmptapd  5375  rdgisucinc  5995  mulidnq  6579  ltrnqg  6610  recexprlem1ssl  6823  recexprlem1ssu  6824  ltmprr  6832  mulcmpblnrlemg  6917  caucvgsrlemoffcau  6974  negsub  7356  neg2sub  7368  divmuleqap  7805  divneg2ap  7824  qapne  8724  binom2  9585  bcpasc  9693  crim  9745  remullem  9758  max0addsup  10105  omeo  10298  sqgcd  10418