Theorem 3eqtr3ri 2641

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  indif2  3829  dfif5  4052  resdm2  5542  co01  5567  funiunfv  6410  dfdom2  7867  1mhlfehlf  11128  crreczi  12851  rei  13744  bpoly3  14628  bpoly4  14629  cos1bnd  14756  rpnnen2lem3  14784  rpnnen2lem11  14792  m1bits  15000  6gcd4e2  15093  3lcm2e6  15278  karatsuba  15630  karatsubaOLD  15631  ring1  18425  sincos4thpi  24069  sincos6thpi  24071  1cubrlem  24368  cht3  24699  bclbnd  24805  bposlem8  24816  ex-ind-dvds  26710  ip1ilem  27065  mdexchi  28578  disjxpin  28783  xppreima  28829  df1stres  28864  df2ndres  28865  xrge0slmod  29175  cnrrext  29382  ballotth  29926  poimirlem3  32582  poimirlem30  32609  mbfposadd  32627  asindmre  32665  areaquad  36821  inductionexd  37473  stoweidlem26  38919  3exp4mod41  40071