Theorem 3eqtr3ri 2767

Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)

Hypotheses

Ref	Expression
3eqtr3i.1	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr3ri

Step	Hyp	Ref	Expression
1		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
2		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
4	2, 3	eqtr3i 2760	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2760	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  indif2  4256  dfif5  4517  resdm2  6220  co01  6250  funiunfv  7240  dfdom2  8992  crreczi  14246  rei  15175  bpoly3  16074  bpoly4  16075  cos1bnd  16205  rpnnen2lem3  16234  rpnnen2lem11  16242  m1bits  16459  6gcd4e2  16557  3lcm2e6  16751  karatsuba  17103  ring1  20270  sincos4thpi  26474  sincos6thpi  26477  1cubrlem  26803  cht3  27135  bclbnd  27243  bposlem8  27254  ex-ind-dvds  30442  ip1ilem  30807  mdexchi  32316  disjxpin  32569  xppreima  32623  df1stres  32681  df2ndres  32682  dpmul100  32871  0dp2dp  32883  dpmul  32887  dpmul4  32888  xrge0slmod  33363  cos9thpiminplylem5  33820  cnrrext  34041  ballotth  34570  hgt750lemd  34680  poimirlem3  37647  poimirlem30  37674  mbfposadd  37691  asindmre  37727  refrelsredund4  38650  420gcd8e4  42019  sqmid3api  42333  areaquad  43240  inductionexd  44179  stoweidlem26  46055  3exp4mod41  47630  tposresg  48853