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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  indif2  4221  dfif5  4483  resdm2  6195  co01  6226  funiunfv  7203  dfdom2  8925  crreczi  14190  rei  15118  bpoly3  16023  bpoly4  16024  cos1bnd  16154  rpnnen2lem3  16183  rpnnen2lem11  16191  m1bits  16409  6gcd4e2  16507  3lcm2e6  16702  karatsuba  17054  ring1  20291  sincos4thpi  26477  sincos6thpi  26480  1cubrlem  26805  cht3  27136  bclbnd  27243  bposlem8  27254  ex-ind-dvds  30531  ip1ilem  30897  mdexchi  32406  disjxpin  32658  xppreima  32718  df1stres  32777  df2ndres  32778  dpmul100  32956  0dp2dp  32968  dpmul  32972  dpmul4  32973  xrge0slmod  33408  cos9thpiminplylem5  33930  cnrrext  34154  ballotth  34682  hgt750lemd  34792  poimirlem3  37944  poimirlem30  37971  mbfposadd  37988  asindmre  38024  refrelsredund4  39037  420gcd8e4  42445  sqmid3api  42715  areaquad  43644  inductionexd  44582  stoweidlem26  46454  3exp4mod41  48079  tposresg  49353