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

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