Theorem 3eqtr3i 2169

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 = C
3eqtr3i.3	|- B = D

Assertion

Ref	Expression
3eqtr3i	|- C = D

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 |- A = B
2		3eqtr3i.2	. . 3 |- A = C
3	1, 2	eqtr3i 2163	. 2 |- B = C
4		3eqtr3i.3	. 2 |- B = D
5	3, 4	eqtr3i 2163	1 |- C = D

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  csbvarg  3035  un12  3239  in12  3292  indif1  3326  difundir  3334  difindir  3336  dif32  3344  resmpt3  4876  xp0  4966  fvsnun1  5625  caov12  5967  caov13  5969  djuassen  7090  xpdjuen  7091  rec1nq  7227  halfnqq  7242  negsubdii  8071  halfpm6th  8964  decmul1  9269  i4  10426  fac4  10511  imi  10704  resqrexlemover  10814  ef01bndlem  11499  znnen  11947  sn0cld  12345  cospi  12929  sincos4thpi  12969  sincos3rdpi  12972  ex-bc  13112  ex-gcd  13114