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

Theorem 3eqtr2ri 2462
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 2458 . 2  |-  A  =  C
4 3eqtr2i.3 . 2  |-  C  =  D
53, 4eqtr2i 2456 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  funimacnv  5517  uniqs  6956  ackbij1lem13  8104  ef01bndlem  12777  cos2bnd  12781  divalglem2  12907  decexp2  13403  lefld  14663  discmp  17453  unmbl  19424  sinhalfpilem  20366  log2cnv  20776  ip0i  22318  polid2i  22651  hh0v  22662  pjinormii  23170  lgam1  24840  subfacp1lem3  24860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator