Theorem 3eqtr3ri 2766

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  indif2  4231  dfif5  4494  resdm2  6187  co01  6218  funiunfv  7192  dfdom2  8913  crreczi  14149  rei  15077  bpoly3  15979  bpoly4  15980  cos1bnd  16110  rpnnen2lem3  16139  rpnnen2lem11  16147  m1bits  16365  6gcd4e2  16463  3lcm2e6  16657  karatsuba  17009  ring1  20243  sincos4thpi  26476  sincos6thpi  26479  1cubrlem  26805  cht3  27137  bclbnd  27245  bposlem8  27256  ex-ind-dvds  30485  ip1ilem  30850  mdexchi  32359  disjxpin  32612  xppreima  32672  df1stres  32732  df2ndres  32733  dpmul100  32927  0dp2dp  32939  dpmul  32943  dpmul4  32944  xrge0slmod  33378  cos9thpiminplylem5  33892  cnrrext  34116  ballotth  34644  hgt750lemd  34754  poimirlem3  37763  poimirlem30  37790  mbfposadd  37807  asindmre  37843  refrelsredund4  38828  420gcd8e4  42199  sqmid3api  42480  areaquad  43400  inductionexd  44338  stoweidlem26  46212  3exp4mod41  47804  tposresg  49065