Theorem 3eqtr2i 2259

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2i.1	⊢ 𝐴 = 𝐵
3eqtr2i.2	⊢ 𝐶 = 𝐵
3eqtr2i.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtr2i	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2256	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2253	1 ⊢ 𝐴 = 𝐷

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 2214

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

This theorem is referenced by:  dfrab3  3497  iunid  4047  cnvcnv  5215  cocnvcnv2  5274  fmptap  5874  exmidfodomrlemim  7504  negdii  8557  halfpm6th  9458  numma  9752  numaddc  9756  6p5lem  9778  8p2e10  9788  binom2i  11010  0.999...  12207  flodddiv4  12622  6gcd4e2  12691  dfphi2  12917  karatsuba  13128  ballotfilem1  13139  cosq23lt0  15698  pigt3  15709  1sgm2ppw  15863  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983  nninfomni  16797