MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtrri Structured version   Unicode version

Theorem 3eqtrri 2436
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtri.1  |-  A  =  B
3eqtri.2  |-  B  =  C
3eqtri.3  |-  C  =  D
Assertion
Ref Expression
3eqtrri  |-  D  =  A

Proof of Theorem 3eqtrri
StepHypRef Expression
1 3eqtri.1 . . 3  |-  A  =  B
2 3eqtri.2 . . 3  |-  B  =  C
31, 2eqtri 2431 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2432 1  |-  D  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394
This theorem is referenced by:  dfif5  3900  difxp1  5249  difxp2  5250  dfdm2  5355  cofunex2g  6748  df1st2  6869  df2nd2  6870  domss2  7713  adderpqlem  9361  dfn2  10848  sqrtm1  13256  0.999...  13840  pockthi  14632  matgsum  19229  indistps  19802  indistps2  19803  refun0  20306  filcon  20674  sincosq3sgn  23183  sincosq4sgn  23184  eff1o  23226  ax5seglem7  24642  clwlknclwlkdifs  25364  cnnvg  25983  cnnvs  25986  cnnvnm  25987  h2hva  26291  h2hsm  26292  h2hnm  26293  hhssva  26575  hhsssm  26576  hhssnm  26577  spansnji  26964  lnopunilem1  27328  lnophmlem2  27335  stadd3i  27566  indifundif  27817  xrsp0  28107  xrsp1  28108  rankeq1o  30496  mbfposadd  31414  iocunico  35522  corcltrcl  35698  binomcxplemdvsum  36088  cosnegpi  37016  fourierdlem62  37300  fouriersw  37363
  Copyright terms: Public domain W3C validator