Theorem 3eqtr3i 2065

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	⊢ A = B
3eqtr3i.2	⊢ A = 𝐶
3eqtr3i.3	⊢ B = 𝐷

Assertion

Ref	Expression
3eqtr3i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 ⊢ A = B
2		3eqtr3i.2	. . 3 ⊢ A = 𝐶
3	1, 2	eqtr3i 2059	. 2 ⊢ B = 𝐶
4		3eqtr3i.3	. 2 ⊢ B = 𝐷
5	3, 4	eqtr3i 2059	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  csbvarg  2871  un12  3095  in12  3142  indif1  3176  difundir  3184  difindir  3186  dif32  3194  resmpt3  4600  xp0  4686  fvsnun1  5303  caov12  5631  caov13  5633  rec1nq  6379  halfnqq  6393  negsubdii  7092  halfpm6th  7922  i4  9008  imi  9128