Theorem 3eqtr3i 2206

Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3i.1	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
3	1, 2	eqtr3i 2200	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2200	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:  csbvarg  3087  un12  3295  in12  3348  indif1  3382  difundir  3390  difindir  3392  dif32  3400  resmpt3  4958  xp0  5050  fvsnun1  5715  caov12  6065  caov13  6067  djuassen  7218  xpdjuen  7219  rec1nq  7396  halfnqq  7411  negsubdii  8244  halfpm6th  9141  decmul1  9449  i4  10625  fac4  10715  imi  10911  resqrexlemover  11021  ef01bndlem  11766  znnen  12401  sn0cld  13722  cospi  14306  sincos4thpi  14346  sincos3rdpi  14349  lgsdir2lem1  14514  lgsdir2lem5  14518  2lgsoddprmlem3d  14543  ex-bc  14566  ex-gcd  14568