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  5850  caov12  6210  caov13  6212  djuassen  7431  xpdjuen  7432  rec1nq  7614  halfnqq  7629  negsubdii  8463  halfpm6th  9363  decmul1  9673  i4  10903  fac4  10994  imi  11460  resqrexlemover  11570  ef01bndlem  12316  modsubi  12991  gcdmodi  12993  numexpp1  12996  karatsuba  13002  znnen  13018  sn0cld  14860  cospi  15523  sincos4thpi  15563  sincos3rdpi  15566  lgsdir2lem1  15756  lgsdir2lem5  15760  2lgsoddprmlem3d  15838  ex-bc  16325  ex-gcd  16327