Theorem 3eqtr3ri 2775

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  indif2  4204  dfif5  4475  resdm2  6134  co01  6165  funiunfv  7121  dfdom2  8766  1mhlfehlf  12192  crreczi  13943  rei  14867  bpoly3  15768  bpoly4  15769  cos1bnd  15896  rpnnen2lem3  15925  rpnnen2lem11  15933  m1bits  16147  6gcd4e2  16246  3lcm2e6  16436  karatsuba  16785  ring1  19841  sincos4thpi  25670  sincos6thpi  25672  1cubrlem  25991  cht3  26322  bclbnd  26428  bposlem8  26439  ex-ind-dvds  28825  ip1ilem  29188  mdexchi  30697  disjxpin  30927  xppreima  30983  df1stres  31036  df2ndres  31037  dpmul100  31171  0dp2dp  31183  dpmul  31187  dpmul4  31188  xrge0slmod  31548  cnrrext  31960  ballotth  32504  hgt750lemd  32628  poimirlem3  35780  poimirlem30  35807  mbfposadd  35824  asindmre  35860  refrelsredund4  36745  420gcd8e4  40014  sqmid3api  40311  areaquad  41047  inductionexd  41765  stoweidlem26  43567  3exp4mod41  45068