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

Theorem 3eqtr2ri 2772
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 2768 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2766 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729
This theorem is referenced by:  funimacnv  6647  uniqs  8817  ackbij1lem13  10271  ef01bndlem  16220  cos2bnd  16224  divalglem2  16432  lefld  18637  smndex2dlinvh  18930  discmp  23406  unmbl  25572  sinhalfpilem  26505  log2cnv  26987  lgam1  27107  ip0i  30844  polid2i  31176  hh0v  31187  pjinormii  31695  dfdec100  32832  dpmul100  32879  dpmul  32895  dpmul4  32896  subfacp1lem3  35187  uniqsALTV  38330  redvmptabs  42390  cotrclrcl  43755  sqwvfoura  46243  sqwvfourb  46244
  Copyright terms: Public domain W3C validator