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  3436  iunid  3969  cnvcnv  5119  cocnvcnv2  5178  fmptap  5749  exmidfodomrlemim  7263  negdii  8305  halfpm6th  9205  numma  9494  numaddc  9498  6p5lem  9520  8p2e10  9530  binom2i  10722  0.999...  11667  flodddiv4  12078  6gcd4e2  12135  dfphi2  12361  cosq23lt0  15009  pigt3  15020  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  nninfomni  15579