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

Theorem 3eqtrri 2850
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 𝐴 = 𝐵
3eqtri.2 𝐵 = 𝐶
3eqtri.3 𝐶 = 𝐷
Assertion
Ref Expression
3eqtrri 𝐷 = 𝐴

Proof of Theorem 3eqtrri
StepHypRef Expression
1 3eqtri.1 . . 3 𝐴 = 𝐵
2 3eqtri.2 . . 3 𝐵 = 𝐶
31, 2eqtri 2845 . 2 𝐴 = 𝐶
4 3eqtri.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2846 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  dfif5  4455  resindm  5878  difxp1  6000  difxp2  6001  dfdm2  6110  cofunex2g  7637  df1st2  7780  df2nd2  7781  domss2  8664  adderpqlem  10365  dfn2  11898  9p1e10  12088  sqrtm1  14626  0.999...  15228  pockthi  16232  matgsum  21040  indistps  21614  indistps2  21615  refun0  22118  filconn  22486  sincosq3sgn  25091  sincosq4sgn  25092  eff1o  25139  ax5seglem7  26727  0grsubgr  27066  nbupgrres  27152  vtxdginducedm1fi  27332  clwwlknclwwlkdif  27762  cnnvg  28459  cnnvs  28461  cnnvnm  28462  h2hva  28755  h2hsm  28756  h2hnm  28757  hhssva  29038  hhsssm  29039  hhssnm  29040  spansnji  29427  lnopunilem1  29791  lnophmlem2  29798  stadd3i  30029  indifundif  30292  dpmul4  30600  xrsp0  30699  xrsp1  30700  hgt750lemd  31993  hgt750lem  31996  rankeq1o  33706  poimirlem8  35023  mbfposadd  35062  iocunico  40091  corcltrcl  40370  binomcxplemdvsum  40993  cosnegpi  42448  fourierdlem62  42749  fouriersw  42812  salexct3  42921  salgensscntex  42923  caragenuncllem  43090  isomenndlem  43108
  Copyright terms: Public domain W3C validator