Theorem 3eqtr2i 2233

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  dfrab3  3453  iunid  3989  cnvcnv  5144  cocnvcnv2  5203  fmptap  5787  exmidfodomrlemim  7325  negdii  8376  halfpm6th  9277  numma  9567  numaddc  9571  6p5lem  9593  8p2e10  9603  binom2i  10815  0.999...  11907  flodddiv4  12322  6gcd4e2  12391  dfphi2  12617  karatsuba  12828  cosq23lt0  15380  pigt3  15391  1sgm2ppw  15542  2lgsoddprmlem3c  15661  2lgsoddprmlem3d  15662  nninfomni  16097