Theorem 3eqtr3i 2234

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 2228	. 2 ⊢ 𝐵 = 𝐶
4		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtr3i 2228	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  csbvarg  3121  un12  3331  in12  3384  indif1  3418  difundir  3426  difindir  3428  dif32  3436  resmpt3  5008  xp0  5102  fvsnun1  5781  caov12  6135  caov13  6137  djuassen  7329  xpdjuen  7330  rec1nq  7508  halfnqq  7523  negsubdii  8357  halfpm6th  9257  decmul1  9567  i4  10787  fac4  10878  imi  11211  resqrexlemover  11321  ef01bndlem  12067  modsubi  12742  gcdmodi  12744  numexpp1  12747  karatsuba  12753  znnen  12769  sn0cld  14609  cospi  15272  sincos4thpi  15312  sincos3rdpi  15315  lgsdir2lem1  15505  lgsdir2lem5  15509  2lgsoddprmlem3d  15587  ex-bc  15669  ex-gcd  15671