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

Theorem 3eqtrri 2807
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 2802 . 2 𝐴 = 𝐶
4 3eqtri.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2803 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771
This theorem is referenced by:  dfif5  4367  resindm  5747  difxp1  5864  difxp2  5865  dfdm2  5972  cofunex2g  7465  df1st2  7603  df2nd2  7604  domss2  8474  adderpqlem  10176  dfn2  11725  9p1e10  11916  sqrtm1  14499  0.999...  15100  pockthi  16102  matgsum  20753  indistps  21326  indistps2  21327  refun0  21830  filconn  22198  sincosq3sgn  24792  sincosq4sgn  24793  eff1o  24837  ax5seglem7  26427  0grsubgr  26766  nbupgrres  26852  vtxdginducedm1fi  27032  clwwlknclwwlkdif  27488  cnnvg  28235  cnnvs  28237  cnnvnm  28238  h2hva  28533  h2hsm  28534  h2hnm  28535  hhssva  28816  hhsssm  28817  hhssnm  28818  spansnji  29207  lnopunilem1  29571  lnophmlem2  29578  stadd3i  29809  indifundif  30062  dpmul4  30339  xrsp0  30400  xrsp1  30401  hgt750lemd  31567  hgt750lem  31570  rankeq1o  33153  poimirlem8  34341  mbfposadd  34380  iocunico  39213  corcltrcl  39447  binomcxplemdvsum  40103  cosnegpi  41579  fourierdlem62  41885  fouriersw  41948  salexct3  42057  salgensscntex  42059  caragenuncllem  42226  isomenndlem  42244
  Copyright terms: Public domain W3C validator