Theorem 3eqtr3i 2236

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  csbvarg  3129  un12  3339  in12  3392  indif1  3426  difundir  3434  difindir  3436  dif32  3444  resmpt3  5027  xp0  5121  fvsnun1  5804  caov12  6158  caov13  6160  djuassen  7360  xpdjuen  7361  rec1nq  7543  halfnqq  7558  negsubdii  8392  halfpm6th  9292  decmul1  9602  i4  10824  fac4  10915  imi  11326  resqrexlemover  11436  ef01bndlem  12182  modsubi  12857  gcdmodi  12859  numexpp1  12862  karatsuba  12868  znnen  12884  sn0cld  14724  cospi  15387  sincos4thpi  15427  sincos3rdpi  15430  lgsdir2lem1  15620  lgsdir2lem5  15624  2lgsoddprmlem3d  15702  ex-bc  15865  ex-gcd  15867