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

Theorem 3eqtr2ri 2323
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  |-  A  =  B
3eqtr2i.2  |-  C  =  B
3eqtr2i.3  |-  C  =  D
Assertion
Ref Expression
3eqtr2ri  |-  D  =  A

Proof of Theorem 3eqtr2ri
StepHypRef Expression
1 3eqtr2i.1 . . 3  |-  A  =  B
2 3eqtr2i.2 . . 3  |-  C  =  B
31, 2eqtr4i 2319 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtr2i 2317 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  funimacnv  5340  uniqs  6735  ackbij1lem13  7874  ef01bndlem  12480  cos2bnd  12484  divalglem2  12610  decexp2  13106  lefld  14364  discmp  17141  unmbl  18911  sinhalfpilem  19850  log2cnv  20256  ip0i  21419  polid2i  21752  hh0v  21763  pjinormii  22271  subfacp1lem3  23728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator