Theorem 3eqtr3i 2199

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

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  csbvarg  3077  un12  3285  in12  3338  indif1  3372  difundir  3380  difindir  3382  dif32  3390  resmpt3  4940  xp0  5030  fvsnun1  5693  caov12  6041  caov13  6043  djuassen  7194  xpdjuen  7195  rec1nq  7357  halfnqq  7372  negsubdii  8204  halfpm6th  9098  decmul1  9406  i4  10578  fac4  10667  imi  10864  resqrexlemover  10974  ef01bndlem  11719  znnen  12353  sn0cld  12931  cospi  13515  sincos4thpi  13555  sincos3rdpi  13558  lgsdir2lem1  13723  lgsdir2lem5  13727  ex-bc  13764  ex-gcd  13766