Theorem 3eqtr2i 2164

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2i.1	|- A = B
3eqtr2i.2	|- C = B
3eqtr2i.3	|- C = D

Assertion

Ref	Expression
3eqtr2i	|- A = D

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 |- A = B
2		3eqtr2i.2	. . 3 |- C = B
3	1, 2	eqtr4i 2161	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2158	1 |- A = D

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  dfrab3  3347  iunid  3863  cnvcnv  4986  cocnvcnv2  5045  fmptap  5603  exmidfodomrlemim  7050  negdii  8039  halfpm6th  8933  numma  9218  numaddc  9222  6p5lem  9244  8p2e10  9254  binom2i  10394  0.999...  11283  flodddiv4  11620  6gcd4e2  11672  dfphi2  11885  txswaphmeolem  12478  cosq23lt0  12903  pigt3  12914  nninfomni  13204