Theorem 3eqtr3i 2267

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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  csbvarg  3175  un12  3387  in12  3442  indif1  3476  difundir  3484  difindir  3486  dif32  3494  resmpt3  5107  xp0  5202  fvsnun1  5903  caov12  6268  caov13  6270  djuassen  7563  xpdjuen  7564  rec1nq  7752  halfnqq  7767  negsubdii  8601  halfpm6th  9504  decmul1  9819  i4  11057  fac4  11149  imi  11644  resqrexlemover  11754  ef01bndlem  12501  modsubi  13176  gcdmodi  13178  numexpp1  13181  karatsuba  13187  ballotfilemth  13259  znnen  13267  sn0cld  15161  cospi  15824  sincos4thpi  15864  sincos3rdpi  15867  lgsdir2lem1  16061  lgsdir2lem5  16065  2lgsoddprmlem3d  16143  ex-bc  16657  ex-gcd  16659