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

Theorem 3eqtr2ri 2856
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr2i.1 𝐴 = 𝐵
3eqtr2i.2 𝐶 = 𝐵
3eqtr2i.3 𝐶 = 𝐷
Assertion
Ref Expression
3eqtr2ri 𝐷 = 𝐴

Proof of Theorem 3eqtr2ri
StepHypRef Expression
1 3eqtr2i.1 . . 3 𝐴 = 𝐵
2 3eqtr2i.2 . . 3 𝐶 = 𝐵
31, 2eqtr4i 2852 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2850 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819
This theorem is referenced by:  funimacnv  6434  uniqs  8352  ackbij1lem13  9648  ef01bndlem  15532  cos2bnd  15536  divalglem2  15741  decexp2  16406  lefld  17831  discmp  21941  unmbl  24072  sinhalfpilem  24983  log2cnv  25455  lgam1  25574  ip0i  28535  polid2i  28867  hh0v  28878  pjinormii  29386  dfdec100  30479  dpmul100  30506  dpmul  30522  dpmul4  30523  subfacp1lem3  32332  uniqsALTV  35473  cotrclrcl  39971  sqwvfoura  42398  sqwvfourb  42399  smndex2dlinvh  43991
  Copyright terms: Public domain W3C validator