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

Theorem 3eqtr2ri 2310
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 2306 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtr2i 2304 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  funimacnv  5324  uniqs  6719  ackbij1lem13  7858  ef01bndlem  12464  cos2bnd  12468  divalglem2  12594  decexp2  13090  lefld  14348  discmp  17125  unmbl  18895  sinhalfpilem  19834  log2cnv  20240  ip0i  21403  polid2i  21736  hh0v  21747  pjinormii  22255  subfacp1lem3  23713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator