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

Theorem 3eqtr2ri 2768
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 2764 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2762 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  funimacnv  6586  uniqs  8722  ackbij1lem13  10176  ef01bndlem  16074  cos2bnd  16078  divalglem2  16285  decexp2  16955  lefld  18489  smndex2dlinvh  18735  discmp  22772  unmbl  24924  sinhalfpilem  25843  log2cnv  26317  lgam1  26436  ip0i  29816  polid2i  30148  hh0v  30159  pjinormii  30667  dfdec100  31782  dpmul100  31809  dpmul  31825  dpmul4  31826  subfacp1lem3  33840  uniqsALTV  36840  cotrclrcl  42106  sqwvfoura  44559  sqwvfourb  44560
  Copyright terms: Public domain W3C validator