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

Theorem 3eqtrri 2678
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 2673 . 2 𝐴 = 𝐶
4 3eqtri.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2674 1 𝐷 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  dfif5  4135  resindm  5479  difxp1  5594  difxp2  5595  dfdm2  5705  cofunex2g  7173  df1st2  7308  df2nd2  7309  domss2  8160  adderpqlem  9814  dfn2  11343  9p1e10  11534  sq10OLD  13091  sqrtm1  14060  0.999...  14656  0.999...OLD  14657  pockthi  15658  matgsum  20291  indistps  20863  indistps2  20864  refun0  21366  filconn  21734  sincosq3sgn  24297  sincosq4sgn  24298  eff1o  24340  ax5seglem7  25860  0grsubgr  26215  nbupgrres  26310  vtxdginducedm1fi  26496  clwwlknclwwlkdif  26945  clwwlknclwwlkdifsOLD  26947  cnnvg  27661  cnnvs  27663  cnnvnm  27664  h2hva  27959  h2hsm  27960  h2hnm  27961  hhssva  28242  hhsssm  28243  hhssnm  28244  spansnji  28633  lnopunilem1  28997  lnophmlem2  29004  stadd3i  29235  indifundif  29482  dpmul4  29750  xrsp0  29809  xrsp1  29810  hgt750lemd  30854  hgt750lem  30857  rankeq1o  32403  poimirlem8  33547  mbfposadd  33587  iocunico  38113  corcltrcl  38348  binomcxplemdvsum  38871  cosnegpi  40396  fourierdlem62  40703  fouriersw  40766  salexct3  40878  salgensscntex  40880  caragenuncllem  41047  isomenndlem  41065
  Copyright terms: Public domain W3C validator