Theorem 3eqtr3i 2225

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 2219	. 2 |- B = C
4		3eqtr3i.3	. 2 |- B = D
5	3, 4	eqtr3i 2219	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbvarg  3112  un12  3321  in12  3374  indif1  3408  difundir  3416  difindir  3418  dif32  3426  resmpt3  4995  xp0  5089  fvsnun1  5759  caov12  6112  caov13  6114  djuassen  7284  xpdjuen  7285  rec1nq  7462  halfnqq  7477  negsubdii  8311  halfpm6th  9211  decmul1  9520  i4  10734  fac4  10825  imi  11065  resqrexlemover  11175  ef01bndlem  11921  modsubi  12588  gcdmodi  12590  numexpp1  12593  karatsuba  12599  znnen  12615  sn0cld  14373  cospi  15036  sincos4thpi  15076  sincos3rdpi  15079  lgsdir2lem1  15269  lgsdir2lem5  15273  2lgsoddprmlem3d  15351  ex-bc  15375  ex-gcd  15377