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

Theorem 3eqtr2ri 2638
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 2634 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2632 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  funimacnv  5870  uniqs  7671  ackbij1lem13  8914  ef01bndlem  14699  cos2bnd  14703  divalglem2  14902  decexp2  15563  lefld  16995  discmp  20953  unmbl  23029  sinhalfpilem  23936  log2cnv  24388  lgam1  24507  ip0i  26870  polid2i  27204  hh0v  27215  pjinormii  27725  subfacp1lem3  30224  cotrclrcl  36849  sqwvfoura  38918  sqwvfourb  38919
  Copyright terms: Public domain W3C validator