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

Theorem eqeq2i 2368
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqeq2i.1  |-  A  =  B
Assertion
Ref Expression
eqeq2i  |-  ( C  =  A  <->  C  =  B )

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2  |-  A  =  B
2 eqeq2 2367 . 2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
31, 2ax-mp 8 1  |-  ( C  =  A  <->  C  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1642
This theorem is referenced by:  eqtri  2378  rabid2  2793  dfss2  3245  equncom  3396  ssunpr  3857  sspr  3858  sstp  3859  preq12b  3869  preqsn  3873  opeqpr  4345  wefrc  4469  orddif  4568  onuninsuci  4713  dfrel4v  5207  dfiota2  5302  funopg  5368  funimaexg  5411  dffn5f  5660  fnressn  5789  fressnfv  5791  fvresex  5848  fnov  6039  elxp6  6238  tpossym  6353  opiota  6377  qsid  6812  mapsncnv  6902  ixpsnf1o  6944  card1  7691  pm54.43lem  7722  cf0  7967  sdom2en01  8018  cardeq0  8264  enqbreq2  8634  addcompr  8735  mulcompr  8737  axrrecex  8875  negeq0  9191  muleqadd  9502  crne0  9829  dfnn3  9850  xmulneg1  10681  hasheq0  11446  hashbc  11487  hashf1lem2  11490  cjne0  11744  sqr00  11845  sqrmsq2i  11967  fsump1i  12329  absefib  12575  efieq1re  12576  xpccatid  14061  isnsg4  14759  2ndcctbss  17287  ptcnp  17422  ovolgelb  18943  ioorinv  19035  rolle  19441  plymul0or  19765  reeff1o  19930  sineq0  19996  coseq1  19997  1cubr  20249  atandm2  20284  atandm3  20285  efrlim  20375  isppw  20464  ppiub  20555  lgsdinn0  20691  m1lgs  20713  isgrpo  20975  vci  21218  chnlei  22178  h1de2ctlem  22248  cmcmlem  22284  cmcm2i  22286  cmbr2i  22289  osumcor2i  22337  pjss2i  22373  ho01i  22522  nmop0h  22685  pjclem1  22889  jplem1  22962  atabs2i  23096  rabid2f  23156  preqsnd  23199  dfrel4  23242  subfacp1lem6  24120  cbvprod  24542  trpredmintr  24792  brdomain  25030  brrange  25031  brimg  25034  brapply  25035  brsuccf  25038  brfullfun  25045  brrestrict  25046  bpoly2  25351  bpoly3  25352  bpoly4  25353  rankeq1o  25360  opropabco  25713  fdc  25779  isdrngo1  25910  smprngopr  26000  mzpcompact2lem  26152  eldioph4b  26217  2nn0ind  26353  islmodfg  26490  elnev  26961  usgra2edg  27556  usgraedg4  27560  usgraidx2vlem1  27564  usgraidx2vlem2  27565  nb3graprlem2  27615  nb3grapr  27616  nb3grapr2  27617  nb3gra2nb  27618  usgrcyclnl2  27765  4cycl4dv  27791  2pthfrgra  27844  bnj168  28520  bnj927  28562  bnj543  28687  bnj970  28741  cdleme25cv  30616  cdlemk35  31170  dicval2  31438  dicopelval2  31440  dicelval2N  31441  hdmap1fval  32056
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2351
  Copyright terms: Public domain W3C validator