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  5843  exmidfodomrlemim  7411  negdii  8462  halfpm6th  9363  numma  9653  numaddc  9657  6p5lem  9679  8p2e10  9689  binom2i  10909  0.999...  12081  flodddiv4  12496  6gcd4e2  12565  dfphi2  12791  karatsuba  13002  cosq23lt0  15556  pigt3  15567  1sgm2ppw  15718  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  nninfomni  16621