Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3ri Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3eqtr3i.3 . 2 𝐵 = 𝐷
2 3eqtr3i.1 . . 3 𝐴 = 𝐵
3 3eqtr3i.2 . . 3 𝐴 = 𝐶
42, 3eqtr3i 2634 . 2 𝐵 = 𝐶
51, 4eqtr3i 2634 1 𝐷 = 𝐶
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator