Theorem 3eqtr3i 2168

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

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  csbvarg  3030  un12  3234  in12  3287  indif1  3321  difundir  3329  difindir  3331  dif32  3339  resmpt3  4868  xp0  4958  fvsnun1  5617  caov12  5959  caov13  5961  djuassen  7073  xpdjuen  7074  rec1nq  7203  halfnqq  7218  negsubdii  8047  halfpm6th  8940  decmul1  9245  i4  10395  fac4  10479  imi  10672  resqrexlemover  10782  ef01bndlem  11463  znnen  11911  sn0cld  12306  cospi  12881  sincos4thpi  12921  sincos3rdpi  12924  ex-bc  12941  ex-gcd  12943