Theorem 3eqtr3ri 2830

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

Syntax hints:   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  indif2  4197  dfif5  4441  resdm2  6055  co01  6081  funiunfv  6985  dfdom2  8518  1mhlfehlf  11844  crreczi  13585  rei  14507  bpoly3  15404  bpoly4  15405  cos1bnd  15532  rpnnen2lem3  15561  rpnnen2lem11  15569  m1bits  15779  6gcd4e2  15876  3lcm2e6  16062  karatsuba  16410  ring1  19348  sincos4thpi  25106  sincos6thpi  25108  1cubrlem  25427  cht3  25758  bclbnd  25864  bposlem8  25875  ex-ind-dvds  28246  ip1ilem  28609  mdexchi  30118  disjxpin  30351  xppreima  30408  df1stres  30463  df2ndres  30464  dpmul100  30599  0dp2dp  30611  dpmul  30615  dpmul4  30616  xrge0slmod  30968  cnrrext  31361  ballotth  31905  hgt750lemd  32029  poimirlem3  35060  poimirlem30  35087  mbfposadd  35104  asindmre  35140  refrelsredund4  36027  420gcd8e4  39294  sqmid3api  39477  areaquad  40166  inductionexd  40858  stoweidlem26  42668  3exp4mod41  44134