Theorem 3eqtr2i 2220

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

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  dfrab3  3435  iunid  3968  cnvcnv  5118  cocnvcnv2  5177  fmptap  5748  exmidfodomrlemim  7261  negdii  8303  halfpm6th  9202  numma  9491  numaddc  9495  6p5lem  9517  8p2e10  9527  binom2i  10719  0.999...  11664  flodddiv4  12075  6gcd4e2  12132  dfphi2  12358  cosq23lt0  14968  pigt3  14979  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198  nninfomni  15509