Theorem 3eqtr2i 2256

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  dfrab3  3481  iunid  4024  cnvcnv  5187  cocnvcnv2  5246  fmptap  5839  exmidfodomrlemim  7402  negdii  8453  halfpm6th  9354  numma  9644  numaddc  9648  6p5lem  9670  8p2e10  9680  binom2i  10900  0.999...  12072  flodddiv4  12487  6gcd4e2  12556  dfphi2  12782  karatsuba  12993  cosq23lt0  15547  pigt3  15558  1sgm2ppw  15709  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  nninfomni  16557