Theorem 3eqtr3ri 2768

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 2761	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2761	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  indif2  4270  dfif5  4544  resdm2  6230  co01  6260  funiunfv  7250  dfdom2  8980  1mhlfehlf  12438  crreczi  14198  rei  15110  bpoly3  16009  bpoly4  16010  cos1bnd  16137  rpnnen2lem3  16166  rpnnen2lem11  16174  m1bits  16388  6gcd4e2  16487  3lcm2e6  16675  karatsuba  17024  ring1  20205  sincos4thpi  26363  sincos6thpi  26365  1cubrlem  26687  cht3  27019  bclbnd  27127  bposlem8  27138  ex-ind-dvds  30148  ip1ilem  30513  mdexchi  32022  disjxpin  32253  xppreima  32305  df1stres  32359  df2ndres  32360  dpmul100  32497  0dp2dp  32509  dpmul  32513  dpmul4  32514  xrge0slmod  32900  cnrrext  33455  ballotth  34001  hgt750lemd  34125  poimirlem3  36957  poimirlem30  36984  mbfposadd  37001  asindmre  37037  refrelsredund4  37968  420gcd8e4  41340  sqmid3api  41660  areaquad  42430  inductionexd  43371  stoweidlem26  45203  3exp4mod41  46745