Theorem 3eqtr3i 2267

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 2261	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2261	1 ⊢ 𝐶 = 𝐷

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  csbvarg  3175  un12  3387  in12  3442  indif1  3476  difundir  3484  difindir  3486  dif32  3494  resmpt3  5115  xp0  5210  fvsnun1  5915  caov12  6281  caov13  6283  djuassen  7580  xpdjuen  7581  rec1nq  7769  halfnqq  7784  negsubdii  8619  halfpm6th  9537  decmul1  9857  i4  11101  fac4  11194  imi  11689  resqrexlemover  11799  ef01bndlem  12549  modsubi  13229  gcdmodi  13231  numexpp1  13234  karatsuba  13240  ballotfilemth  13340  znnen  13348  sn0cld  15375  cospi  16039  sincos4thpi  16079  sincos3rdpi  16082  log2ublem2  16234  log2ublog2  16236  chtqub  16308  bclbnd  16319  bposlem8  16330  lgsdir2lem1  16364  lgsdir2lem5  16368  2lgsoddprmlem3d  16446  ex-bc  16960  ex-gcd  16962