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  5112  xp0  5207  fvsnun1  5912  caov12  6278  caov13  6280  djuassen  7573  xpdjuen  7574  rec1nq  7762  halfnqq  7777  negsubdii  8611  halfpm6th  9527  decmul1  9842  i4  11081  fac4  11173  imi  11668  resqrexlemover  11778  ef01bndlem  12525  modsubi  13200  gcdmodi  13202  numexpp1  13205  karatsuba  13211  ballotfilemth  13283  znnen  13291  sn0cld  15240  cospi  15904  sincos4thpi  15944  sincos3rdpi  15947  log2ublem2  16090  log2ublog2  16092  bclbnd  16127  lgsdir2lem1  16159  lgsdir2lem5  16163  2lgsoddprmlem3d  16241  ex-bc  16755  ex-gcd  16757