Theorem 3eqtr3i 2263

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  csbvarg  3168  un12  3379  in12  3434  indif1  3468  difundir  3476  difindir  3478  dif32  3486  resmpt3  5089  xp0  5184  fvsnun1  5883  caov12  6245  caov13  6247  djuassen  7526  xpdjuen  7527  rec1nq  7715  halfnqq  7730  negsubdii  8563  halfpm6th  9463  decmul1  9778  i4  11011  fac4  11103  imi  11593  resqrexlemover  11703  ef01bndlem  12450  modsubi  13125  gcdmodi  13127  numexpp1  13130  karatsuba  13136  znnen  13170  sn0cld  15051  cospi  15714  sincos4thpi  15754  sincos3rdpi  15757  lgsdir2lem1  15950  lgsdir2lem5  15954  2lgsoddprmlem3d  16032  ex-bc  16546  ex-gcd  16548