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

Theorem 3eqtrri 2766
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 2761 . 2 𝐴 = 𝐶
4 3eqtri.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2762 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  dfif5  4506  resindm  5990  difxp1  6121  difxp2  6122  dfdm2  6237  cofunex2g  7886  df1st2  8034  df2nd2  8035  domss2  9086  adderpqlem  10898  dfn2  12434  9p1e10  12628  sqrtm1  15169  0.999...  15774  pockthi  16787  matgsum  21809  indistps  22384  indistps2  22385  refun0  22889  filconn  23257  sincosq3sgn  25880  sincosq4sgn  25881  eff1o  25928  ax5seglem7  27933  0grsubgr  28275  nbupgrres  28361  vtxdginducedm1fi  28541  clwwlknclwwlkdif  28972  cnnvg  29669  cnnvs  29671  cnnvnm  29672  h2hva  29965  h2hsm  29966  h2hnm  29967  hhssva  30248  hhsssm  30249  hhssnm  30250  spansnji  30637  lnopunilem1  31001  lnophmlem2  31008  stadd3i  31239  indifundif  31502  dpmul4  31826  xrsp0  31928  xrsp1  31929  hgt750lemd  33325  hgt750lem  33328  rankeq1o  34809  poimirlem8  36136  mbfposadd  36175  iocunico  41592  corcltrcl  42103  binomcxplemdvsum  42727  cosnegpi  44198  fourierdlem62  44499  fouriersw  44562  salexct3  44673  salgensscntex  44675  caragenuncllem  44843  isomenndlem  44861
  Copyright terms: Public domain W3C validator