Theorem 3eqtr2i 2234

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 2231	. 2 |- A = C
4		3eqtr2i.3	. 2 |- C = D
5	3, 4	eqtri 2228	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  dfrab3  3457  iunid  3997  cnvcnv  5154  cocnvcnv2  5213  fmptap  5797  exmidfodomrlemim  7340  negdii  8391  halfpm6th  9292  numma  9582  numaddc  9586  6p5lem  9608  8p2e10  9618  binom2i  10830  0.999...  11947  flodddiv4  12362  6gcd4e2  12431  dfphi2  12657  karatsuba  12868  cosq23lt0  15420  pigt3  15431  1sgm2ppw  15582  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  nninfomni  16158