Theorem 3eqtr2i 2258

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 2255	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2252	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  dfrab3  3483  iunid  4026  cnvcnv  5189  cocnvcnv2  5248  fmptap  5844  exmidfodomrlemim  7412  negdii  8463  halfpm6th  9364  numma  9654  numaddc  9658  6p5lem  9680  8p2e10  9690  binom2i  10911  0.999...  12100  flodddiv4  12515  6gcd4e2  12584  dfphi2  12810  karatsuba  13021  cosq23lt0  15576  pigt3  15587  1sgm2ppw  15738  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858  nninfomni  16672