Theorem 3eqtr3i 2206

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  csbvarg  3086  un12  3294  in12  3347  indif1  3381  difundir  3389  difindir  3391  dif32  3399  resmpt3  4957  xp0  5049  fvsnun1  5714  caov12  6063  caov13  6065  djuassen  7216  xpdjuen  7217  rec1nq  7394  halfnqq  7409  negsubdii  8242  halfpm6th  9139  decmul1  9447  i4  10623  fac4  10713  imi  10909  resqrexlemover  11019  ef01bndlem  11764  znnen  12399  sn0cld  13640  cospi  14224  sincos4thpi  14264  sincos3rdpi  14267  lgsdir2lem1  14432  lgsdir2lem5  14436  2lgsoddprmlem3d  14461  ex-bc  14484  ex-gcd  14486