Theorem 3eqtr2i 2192

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  dfrab3  3398  iunid  3921  cnvcnv  5056  cocnvcnv2  5115  fmptap  5675  exmidfodomrlemim  7157  negdii  8182  halfpm6th  9077  numma  9365  numaddc  9369  6p5lem  9391  8p2e10  9401  binom2i  10563  0.999...  11462  flodddiv4  11871  6gcd4e2  11928  dfphi2  12152  txswaphmeolem  12960  cosq23lt0  13394  pigt3  13405  nninfomni  13899