Theorem 3eqtr2i 2223

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  dfrab3  3440  iunid  3973  cnvcnv  5123  cocnvcnv2  5182  fmptap  5755  exmidfodomrlemim  7280  negdii  8327  halfpm6th  9228  numma  9517  numaddc  9521  6p5lem  9543  8p2e10  9553  binom2i  10757  0.999...  11703  flodddiv4  12118  6gcd4e2  12187  dfphi2  12413  karatsuba  12624  cosq23lt0  15153  pigt3  15164  1sgm2ppw  15315  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  nninfomni  15750