Theorem 3eqtr3i 2234

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  csbvarg  3121  un12  3331  in12  3384  indif1  3418  difundir  3426  difindir  3428  dif32  3436  resmpt3  5009  xp0  5103  fvsnun1  5783  caov12  6137  caov13  6139  djuassen  7331  xpdjuen  7332  rec1nq  7510  halfnqq  7525  negsubdii  8359  halfpm6th  9259  decmul1  9569  i4  10789  fac4  10880  imi  11244  resqrexlemover  11354  ef01bndlem  12100  modsubi  12775  gcdmodi  12777  numexpp1  12780  karatsuba  12786  znnen  12802  sn0cld  14642  cospi  15305  sincos4thpi  15345  sincos3rdpi  15348  lgsdir2lem1  15538  lgsdir2lem5  15542  2lgsoddprmlem3d  15620  ex-bc  15702  ex-gcd  15704