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

Theorem 3eqtrri 2321
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 2316 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2317 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  dfif5  3590  dfdm2  5220  cofunex2g  5756  difxp1  6170  difxp2  6171  df1st2  6221  df2nd2  6222  domss2  7036  adderpqlem  8594  dfn2  9994  sqrm1  11777  0.999...  12353  pockthi  12970  indistps  16764  indistps2  16765  filcon  17594  sincosq3sgn  19884  sincosq4sgn  19885  eff1o  19927  cnnvg  21262  cnnvs  21265  cnnvnm  21266  h2hva  21570  h2hsm  21571  h2hnm  21572  hhssva  21852  hhsssm  21853  hhssnm  21854  spansnji  22241  lnopunilem1  22606  stadd3i  22844  ax5seglem7  24635  rankeq1o  24873  dispos  25390  wlkntrllem1  28345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator