Theorem 3eqtr3i 2194

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  csbvarg  3073  un12  3280  in12  3333  indif1  3367  difundir  3375  difindir  3377  dif32  3385  resmpt3  4933  xp0  5023  fvsnun1  5682  caov12  6030  caov13  6032  djuassen  7173  xpdjuen  7174  rec1nq  7336  halfnqq  7351  negsubdii  8183  halfpm6th  9077  decmul1  9385  i4  10557  fac4  10646  imi  10842  resqrexlemover  10952  ef01bndlem  11697  znnen  12331  sn0cld  12787  cospi  13371  sincos4thpi  13411  sincos3rdpi  13414  lgsdir2lem1  13579  lgsdir2lem5  13583  ex-bc  13620  ex-gcd  13622