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

Theorem 3eqtrri 2468
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 2463 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2464 1  |-  D  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  dfif5  3810  difxp1  5268  difxp2  5269  dfdm2  5374  cofunex2g  6547  df1st2  6664  df2nd2  6665  domss2  7475  adderpqlem  9128  dfn2  10597  sqrm1  12770  0.999...  13346  pockthi  13973  indistps  18620  indistps2  18621  filcon  19461  sincosq3sgn  21967  sincosq4sgn  21968  eff1o  22010  ax5seglem7  23186  cnnvg  24073  cnnvs  24076  cnnvnm  24077  h2hva  24381  h2hsm  24382  h2hnm  24383  hhssva  24665  hhsssm  24666  hhssnm  24667  spansnji  25054  lnopunilem1  25419  lnophmlem2  25426  stadd3i  25657  xrsp0  26147  xrsp1  26148  rankeq1o  28214  mbfposadd  28444  iocunico  29591  clwlknclwlkdifs  30583  matgsum  30867
  Copyright terms: Public domain W3C validator