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 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  csbvarg  3175  un12  3387  in12  3442  indif1  3476  difundir  3484  difindir  3486  dif32  3494  resmpt3  5110  xp0  5205  fvsnun1  5906  caov12  6272  caov13  6274  djuassen  7567  xpdjuen  7568  rec1nq  7756  halfnqq  7771  negsubdii  8605  halfpm6th  9508  decmul1  9823  i4  11062  fac4  11154  imi  11649  resqrexlemover  11759  ef01bndlem  12506  modsubi  13181  gcdmodi  13183  numexpp1  13186  karatsuba  13192  ballotfilemth  13264  znnen  13272  sn0cld  15221  cospi  15884  sincos4thpi  15924  sincos3rdpi  15927  log2ublem2  16067  log2ublog2  16069  lgsdir2lem1  16130  lgsdir2lem5  16134  2lgsoddprmlem3d  16212  ex-bc  16726  ex-gcd  16728