Theorem 3eqtr3i 2222

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

Syntax hints:   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186

This theorem is referenced by:  csbvarg  3109  un12  3318  in12  3371  indif1  3405  difundir  3413  difindir  3415  dif32  3423  resmpt3  4992  xp0  5086  fvsnun1  5756  caov12  6109  caov13  6111  djuassen  7279  xpdjuen  7280  rec1nq  7457  halfnqq  7472  negsubdii  8306  halfpm6th  9205  decmul1  9514  i4  10716  fac4  10807  imi  11047  resqrexlemover  11157  ef01bndlem  11902  znnen  12558  sn0cld  14316  cospi  14976  sincos4thpi  15016  sincos3rdpi  15019  lgsdir2lem1  15185  lgsdir2lem5  15189  2lgsoddprmlem3d  15267  ex-bc  15291  ex-gcd  15293