Theorem 3eqtr3i 2260

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  csbvarg  3155  un12  3365  in12  3418  indif1  3452  difundir  3460  difindir  3462  dif32  3470  resmpt3  5062  xp0  5156  fvsnun1  5851  caov12  6211  caov13  6213  djuassen  7432  xpdjuen  7433  rec1nq  7615  halfnqq  7630  negsubdii  8464  halfpm6th  9364  decmul1  9674  i4  10905  fac4  10996  imi  11478  resqrexlemover  11588  ef01bndlem  12335  modsubi  13010  gcdmodi  13012  numexpp1  13015  karatsuba  13021  znnen  13037  sn0cld  14880  cospi  15543  sincos4thpi  15583  sincos3rdpi  15586  lgsdir2lem1  15776  lgsdir2lem5  15780  2lgsoddprmlem3d  15858  ex-bc  16372  ex-gcd  16374