Theorem 3eqtr3ri 2768

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  indif2  4233  dfif5  4496  resdm2  6189  co01  6220  funiunfv  7194  dfdom2  8915  crreczi  14151  rei  15079  bpoly3  15981  bpoly4  15982  cos1bnd  16112  rpnnen2lem3  16141  rpnnen2lem11  16149  m1bits  16367  6gcd4e2  16465  3lcm2e6  16659  karatsuba  17011  ring1  20245  sincos4thpi  26478  sincos6thpi  26481  1cubrlem  26807  cht3  27139  bclbnd  27247  bposlem8  27258  ex-ind-dvds  30536  ip1ilem  30901  mdexchi  32410  disjxpin  32663  xppreima  32723  df1stres  32783  df2ndres  32784  dpmul100  32978  0dp2dp  32990  dpmul  32994  dpmul4  32995  xrge0slmod  33429  cos9thpiminplylem5  33943  cnrrext  34167  ballotth  34695  hgt750lemd  34805  poimirlem3  37824  poimirlem30  37851  mbfposadd  37868  asindmre  37904  refrelsredund4  38889  420gcd8e4  42260  sqmid3api  42538  areaquad  43458  inductionexd  44396  stoweidlem26  46270  3exp4mod41  47862  tposresg  49123