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

Theorem 3eqtr2ri 2789
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 2785 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2783 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753
This theorem is referenced by:  funimacnv  6131  uniqs  7976  ackbij1lem13  9266  ef01bndlem  15133  cos2bnd  15137  divalglem2  15340  decexp2  16001  lefld  17447  discmp  21423  unmbl  23525  sinhalfpilem  24435  log2cnv  24891  lgam1  25010  ip0i  28010  polid2i  28344  hh0v  28355  pjinormii  28865  dfdec100  29906  dpmul100  29935  dpmul  29951  dpmul4  29952  subfacp1lem3  31492  uniqsALTV  34443  cotrclrcl  38554  sqwvfoura  40966  sqwvfourb  40967
  Copyright terms: Public domain W3C validator