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

Theorem 3eqtr2ri 2479
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 2475 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtr2i 2473 1  |-  D  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  funimacnv  5650  uniqs  7373  ackbij1lem13  8615  ef01bndlem  13901  cos2bnd  13905  divalglem2  14035  decexp2  14543  lefld  15835  discmp  19876  unmbl  21926  sinhalfpilem  22834  log2cnv  23253  ip0i  25718  polid2i  26052  hh0v  26063  pjinormii  26572  lgam1  28584  subfacp1lem3  28604  sqwvfoura  31965  sqwvfourb  31966
  Copyright terms: Public domain W3C validator