Theorem 3eqtr3i 2218

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 2212	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2212	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  csbvarg  3100  un12  3308  in12  3361  indif1  3395  difundir  3403  difindir  3405  dif32  3413  resmpt3  4974  xp0  5066  fvsnun1  5733  caov12  6084  caov13  6086  djuassen  7245  xpdjuen  7246  rec1nq  7423  halfnqq  7438  negsubdii  8271  halfpm6th  9168  decmul1  9476  i4  10653  fac4  10744  imi  10940  resqrexlemover  11050  ef01bndlem  11795  znnen  12448  sn0cld  14089  cospi  14673  sincos4thpi  14713  sincos3rdpi  14716  lgsdir2lem1  14882  lgsdir2lem5  14886  2lgsoddprmlem3d  14911  ex-bc  14934  ex-gcd  14936