Theorem 3eqtr3i 2225

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbvarg  3112  un12  3322  in12  3375  indif1  3409  difundir  3417  difindir  3419  dif32  3427  resmpt3  4996  xp0  5090  fvsnun1  5762  caov12  6116  caov13  6118  djuassen  7302  xpdjuen  7303  rec1nq  7481  halfnqq  7496  negsubdii  8330  halfpm6th  9230  decmul1  9539  i4  10753  fac4  10844  imi  11084  resqrexlemover  11194  ef01bndlem  11940  modsubi  12615  gcdmodi  12617  numexpp1  12620  karatsuba  12626  znnen  12642  sn0cld  14481  cospi  15144  sincos4thpi  15184  sincos3rdpi  15187  lgsdir2lem1  15377  lgsdir2lem5  15381  2lgsoddprmlem3d  15459  ex-bc  15483  ex-gcd  15485