Theorem 3eqtr3i 2109

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 2103	. 2 |- B = C
4		3eqtr3i.3	. 2 |- B = D
5	3, 4	eqtr3i 2103	1 |- C = D

Syntax hints:   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  csbvarg  2933  un12  3130  in12  3177  indif1  3209  difundir  3217  difindir  3219  dif32  3227  resmpt3  4677  xp0  4763  fvsnun1  5381  caov12  5709  caov13  5711  rec1nq  6585  halfnqq  6600  negsubdii  7393  halfpm6th  8251  decmul1  8540  i4  9577  fac4  9660  imi  9787  resqrexlemover  9896  ex-bc  10566  ex-gcd  10568