Theorem 3eqtr2i 2265

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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  dfrab3  3509  iunid  4063  cnvcnv  5235  cocnvcnv2  5294  fmptap  5896  exmidfodomrlemim  7543  negdii  8600  halfpm6th  9504  numma  9799  numaddc  9803  6p5lem  9825  8p2e10  9835  binom2i  11063  0.999...  12266  flodddiv4  12681  6gcd4e2  12750  dfphi2  12976  karatsuba  13187  ballotfilem1  13198  ballotfilemfval0  13213  ballotfilemth  13259  cosq23lt0  15857  pigt3  15868  1sgm2ppw  16023  2lgsoddprmlem3c  16142  2lgsoddprmlem3d  16143  nninfomni  16967