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

Theorem 3eqtr2ri 2639
 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 𝐴 = 𝐵
3eqtr2i.2 𝐶 = 𝐵
3eqtr2i.3 𝐶 = 𝐷
Assertion
Ref Expression
3eqtr2ri 𝐷 = 𝐴

Proof of Theorem 3eqtr2ri
StepHypRef Expression
1 3eqtr2i.1 . . 3 𝐴 = 𝐵
2 3eqtr2i.2 . . 3 𝐶 = 𝐵
31, 2eqtr4i 2635 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2633 1 𝐷 = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603 This theorem is referenced by:  funimacnv  5884  uniqs  7694  ackbij1lem13  8937  ef01bndlem  14753  cos2bnd  14757  divalglem2  14956  decexp2  15617  lefld  17049  discmp  21011  unmbl  23112  sinhalfpilem  24019  log2cnv  24471  lgam1  24590  ip0i  27064  polid2i  27398  hh0v  27409  pjinormii  27919  subfacp1lem3  30418  cotrclrcl  37053  sqwvfoura  39121  sqwvfourb  39122
 Copyright terms: Public domain W3C validator