Theorem 3eqtr2i 2232

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  dfrab3  3449  iunid  3983  cnvcnv  5136  cocnvcnv2  5195  fmptap  5776  exmidfodomrlemim  7311  negdii  8358  halfpm6th  9259  numma  9549  numaddc  9553  6p5lem  9575  8p2e10  9585  binom2i  10795  0.999...  11865  flodddiv4  12280  6gcd4e2  12349  dfphi2  12575  karatsuba  12786  cosq23lt0  15338  pigt3  15349  1sgm2ppw  15500  2lgsoddprmlem3c  15619  2lgsoddprmlem3d  15620  nninfomni  15993