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  4244  dfif5  4505  resdm2  6204  co01  6234  funiunfv  7222  dfdom2  8949  crreczi  14193  rei  15122  bpoly3  16024  bpoly4  16025  cos1bnd  16155  rpnnen2lem3  16184  rpnnen2lem11  16192  m1bits  16410  6gcd4e2  16508  3lcm2e6  16702  karatsuba  17054  ring1  20219  sincos4thpi  26422  sincos6thpi  26425  1cubrlem  26751  cht3  27083  bclbnd  27191  bposlem8  27202  ex-ind-dvds  30390  ip1ilem  30755  mdexchi  32264  disjxpin  32517  xppreima  32569  df1stres  32627  df2ndres  32628  dpmul100  32817  0dp2dp  32829  dpmul  32833  dpmul4  32834  xrge0slmod  33319  cos9thpiminplylem5  33776  cnrrext  34000  ballotth  34529  hgt750lemd  34639  poimirlem3  37617  poimirlem30  37644  mbfposadd  37661  asindmre  37697  refrelsredund4  38623  420gcd8e4  41994  sqmid3api  42271  areaquad  43205  inductionexd  44144  stoweidlem26  46024  3exp4mod41  47617  tposresg  48866