Theorem 3eqtr3i 2233

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

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  csbvarg  3120  un12  3330  in12  3383  indif1  3417  difundir  3425  difindir  3427  dif32  3435  resmpt3  5007  xp0  5101  fvsnun1  5780  caov12  6134  caov13  6136  djuassen  7328  xpdjuen  7329  rec1nq  7507  halfnqq  7522  negsubdii  8356  halfpm6th  9256  decmul1  9566  i4  10785  fac4  10876  imi  11182  resqrexlemover  11292  ef01bndlem  12038  modsubi  12713  gcdmodi  12715  numexpp1  12718  karatsuba  12724  znnen  12740  sn0cld  14580  cospi  15243  sincos4thpi  15283  sincos3rdpi  15286  lgsdir2lem1  15476  lgsdir2lem5  15480  2lgsoddprmlem3d  15558  ex-bc  15627  ex-gcd  15629