Theorem 3eqtr2i 2197

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

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  dfrab3  3403  iunid  3928  cnvcnv  5063  cocnvcnv2  5122  fmptap  5686  exmidfodomrlemim  7178  negdii  8203  halfpm6th  9098  numma  9386  numaddc  9390  6p5lem  9412  8p2e10  9422  binom2i  10584  0.999...  11484  flodddiv4  11893  6gcd4e2  11950  dfphi2  12174  txswaphmeolem  13114  cosq23lt0  13548  pigt3  13559  nninfomni  14052