Theorem 3eqtr2i 2166

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 2163	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2160	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 2121

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

This theorem is referenced by:  dfrab3  3352  iunid  3868  cnvcnv  4991  cocnvcnv2  5050  fmptap  5610  exmidfodomrlemim  7057  negdii  8046  halfpm6th  8940  numma  9225  numaddc  9229  6p5lem  9251  8p2e10  9261  binom2i  10401  0.999...  11290  flodddiv4  11631  6gcd4e2  11683  dfphi2  11896  txswaphmeolem  12489  cosq23lt0  12914  pigt3  12925  nninfomni  13215