Theorem 3eqtr2i 2265

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  dfrab3  3509  iunid  4068  cnvcnv  5243  cocnvcnv2  5302  fmptap  5908  exmidfodomrlemim  7559  negdii  8617  halfpm6th  9536  numma  9836  numaddc  9840  6p5lem  9862  8p2e10  9872  binom2i  11106  0.999...  12313  flodddiv4  12728  6gcd4e2  12797  dfphi2  13027  mod2xnegi  13227  karatsuba  13239  1259lem1  13271  ballotfilem1  13278  ballotfilemfval0  13293  ballotfilemth  13339  cosq23lt0  16060  pigt3  16071  log2ublem3  16223  1sgm2ppw  16289  ppiqub  16293  bposlem8  16318  bposlem9  16319  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434  nninfomni  17268