Theorem 3eqtr2i 2204

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  dfrab3  3413  iunid  3944  cnvcnv  5083  cocnvcnv2  5142  fmptap  5708  exmidfodomrlemim  7202  negdii  8243  halfpm6th  9141  numma  9429  numaddc  9433  6p5lem  9455  8p2e10  9465  binom2i  10631  0.999...  11531  flodddiv4  11941  6gcd4e2  11998  dfphi2  12222  txswaphmeolem  13905  cosq23lt0  14339  pigt3  14350  2lgsoddprmlem3c  14542  2lgsoddprmlem3d  14543  nninfomni  14853