Theorem 3eqtr2i 2261

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  dfrab3  3499  iunid  4049  cnvcnv  5217  cocnvcnv2  5276  fmptap  5876  exmidfodomrlemim  7506  negdii  8559  halfpm6th  9460  numma  9755  numaddc  9759  6p5lem  9781  8p2e10  9791  binom2i  11014  0.999...  12211  flodddiv4  12626  6gcd4e2  12695  dfphi2  12921  karatsuba  13132  ballotfilem1  13143  ballotfilemfval0  13156  cosq23lt0  15715  pigt3  15726  1sgm2ppw  15880  2lgsoddprmlem3c  15999  2lgsoddprmlem3d  16000  nninfomni  16814