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

Theorem 3eqtr2ri 2496
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 2492 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtr2i 2490 1  |-  D  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-cleq 2452
This theorem is referenced by:  funimacnv  5651  uniqs  7361  ackbij1lem13  8601  ef01bndlem  13769  cos2bnd  13773  divalglem2  13901  decexp2  14409  lefld  15702  discmp  19657  unmbl  21676  sinhalfpilem  22582  log2cnv  22996  ip0i  25402  polid2i  25736  hh0v  25747  pjinormii  26256  lgam1  28232  subfacp1lem3  28252
  Copyright terms: Public domain W3C validator