Theorem 3eqtr2i 2231

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

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  dfrab3  3448  iunid  3982  cnvcnv  5134  cocnvcnv2  5193  fmptap  5773  exmidfodomrlemim  7308  negdii  8355  halfpm6th  9256  numma  9546  numaddc  9550  6p5lem  9572  8p2e10  9582  binom2i  10791  0.999...  11774  flodddiv4  12189  6gcd4e2  12258  dfphi2  12484  karatsuba  12695  cosq23lt0  15247  pigt3  15258  1sgm2ppw  15409  2lgsoddprmlem3c  15528  2lgsoddprmlem3d  15529  nninfomni  15889