Theorem 3eqtr3ri 2761

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 2754	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2754	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  indif2  4232  dfif5  4493  resdm2  6180  co01  6210  funiunfv  7184  dfdom2  8903  crreczi  14135  rei  15063  bpoly3  15965  bpoly4  15966  cos1bnd  16096  rpnnen2lem3  16125  rpnnen2lem11  16133  m1bits  16351  6gcd4e2  16449  3lcm2e6  16643  karatsuba  16995  ring1  20195  sincos4thpi  26420  sincos6thpi  26423  1cubrlem  26749  cht3  27081  bclbnd  27189  bposlem8  27200  ex-ind-dvds  30405  ip1ilem  30770  mdexchi  32279  disjxpin  32532  xppreima  32588  df1stres  32646  df2ndres  32647  dpmul100  32837  0dp2dp  32849  dpmul  32853  dpmul4  32854  xrge0slmod  33285  cos9thpiminplylem5  33753  cnrrext  33977  ballotth  34506  hgt750lemd  34616  poimirlem3  37603  poimirlem30  37630  mbfposadd  37647  asindmre  37683  refrelsredund4  38609  420gcd8e4  41979  sqmid3api  42256  areaquad  43189  inductionexd  44128  stoweidlem26  46007  3exp4mod41  47600  tposresg  48862