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  5240  cocnvcnv2  5299  fmptap  5905  exmidfodomrlemim  7553  negdii  8610  halfpm6th  9525  numma  9820  numaddc  9824  6p5lem  9846  8p2e10  9856  binom2i  11085  0.999...  12288  flodddiv4  12703  6gcd4e2  12772  dfphi2  12998  karatsuba  13209  ballotfilem1  13220  ballotfilemfval0  13235  ballotfilemth  13281  cosq23lt0  15934  pigt3  15945  log2ublem3  16085  1sgm2ppw  16109  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  nninfomni  17062