Theorem 3eqtr3i 2261

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  csbvarg  3166  un12  3377  in12  3432  indif1  3466  difundir  3474  difindir  3476  dif32  3484  resmpt3  5087  xp0  5182  fvsnun1  5881  caov12  6243  caov13  6245  djuassen  7524  xpdjuen  7525  rec1nq  7710  halfnqq  7725  negsubdii  8558  halfpm6th  9458  decmul1  9772  i4  11004  fac4  11095  imi  11585  resqrexlemover  11695  ef01bndlem  12442  modsubi  13117  gcdmodi  13119  numexpp1  13122  karatsuba  13128  znnen  13149  sn0cld  15002  cospi  15665  sincos4thpi  15705  sincos3rdpi  15708  lgsdir2lem1  15901  lgsdir2lem5  15905  2lgsoddprmlem3d  15983  ex-bc  16497  ex-gcd  16499