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

Theorem 3eqtr2ri 2680
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 2676 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2674 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  funimacnv  6008  uniqs  7850  ackbij1lem13  9092  ef01bndlem  14958  cos2bnd  14962  divalglem2  15165  decexp2  15826  lefld  17273  discmp  21249  unmbl  23351  sinhalfpilem  24260  log2cnv  24716  lgam1  24835  ip0i  27808  polid2i  28142  hh0v  28153  pjinormii  28663  dfdec100  29704  dpmul100  29733  dpmul  29749  dpmul4  29750  subfacp1lem3  31290  uniqsALTV  34242  cotrclrcl  38351  sqwvfoura  40763  sqwvfourb  40764
  Copyright terms: Public domain W3C validator