Theorem 3eqtr3i 2199

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	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr3i

Step	Hyp	Ref	Expression
1		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
3	1, 2	eqtr3i 2193	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2193	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  csbvarg  3077  un12  3285  in12  3338  indif1  3372  difundir  3380  difindir  3382  dif32  3390  resmpt3  4938  xp0  5028  fvsnun1  5690  caov12  6038  caov13  6040  djuassen  7181  xpdjuen  7182  rec1nq  7344  halfnqq  7359  negsubdii  8191  halfpm6th  9085  decmul1  9393  i4  10565  fac4  10654  imi  10851  resqrexlemover  10961  ef01bndlem  11706  znnen  12340  sn0cld  12852  cospi  13436  sincos4thpi  13476  sincos3rdpi  13479  lgsdir2lem1  13644  lgsdir2lem5  13648  ex-bc  13685  ex-gcd  13687