Theorem 3eqtr2i 2197

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 2194	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2191	1 |- A = D

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  dfrab3  3403  iunid  3926  cnvcnv  5061  cocnvcnv2  5120  fmptap  5683  exmidfodomrlemim  7165  negdii  8190  halfpm6th  9085  numma  9373  numaddc  9377  6p5lem  9399  8p2e10  9409  binom2i  10571  0.999...  11471  flodddiv4  11880  6gcd4e2  11937  dfphi2  12161  txswaphmeolem  13035  cosq23lt0  13469  pigt3  13480  nninfomni  13974