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

Theorem eqeq2i 2475
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
eqeq2i.1
Assertion
Ref Expression
eqeq2i

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2
2 eqeq2 2472 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395
This theorem is referenced by:  eqeq12i  2477  eqtri  2486  neeq2i  2744  rabid2  3035  dfss2  3492  equncom  3648  rabrsn  4100  ssunpr  4192  sspr  4193  sstp  4194  preq12b  4206  preqsn  4213  opeqpr  4749  wefrc  4878  orddif  4976  dfrel4v  5463  dfiota2  5557  funopg  5625  funimaexg  5670  dffn5f  5928  fnressn  6083  fressnfv  6085  fnprb  6129  fnov  6410  ovmpt2s  6426  onuninsuci  6675  fvresex  6773  elxp6  6832  el2xptp  6843  el2xptp0  6844  opiota  6859  tpossym  7006  qsid  7396  mapsncnv  7485  ixpsnf1o  7529  card1  8370  pm54.43lem  8401  cf0  8652  sdom2en01  8703  cardeq0  8948  enqbreq2  9319  addcompr  9420  mulcompr  9422  axrrecex  9561  negeq0  9896  muleqadd  10218  crne0  10554  dfnn3  10575  xmulneg1  11490  hasheq0  12433  hashbc  12502  hashf1lem2  12505  hash2pwpr  12519  cjne0  12996  sqrt00  13097  sqrtmsq2i  13220  cbvsum  13517  fsump1i  13584  cbvprod  13722  absefib  13933  efieq1re  13934  xpccatid  15457  isnsg4  16244  mat1dimelbas  18973  pmatcollpw3fi1lem1  19287  2ndcctbss  19956  ptcnp  20123  ovolgelb  21891  ioorinv  21985  rolle  22391  plymul0or  22677  reeff1o  22842  sineq0  22914  coseq1  22915  1cubr  23173  atandm2  23208  atandm3  23209  efrlim  23299  isppw  23388  ppiub  23479  lgsdinn0  23615  m1lgs  23637  usgra2edg  24382  usgraedg4  24387  usgraidx2vlem1  24391  usgraidx2vlem2  24392  nb3graprlem2  24452  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  2trllemH  24554  2trllemE  24555  usgrcyclnl2  24641  4cycl4dv  24667  wwlkn0  24689  wwlkn0s  24705  rusgranumwlkl1  24947  2pthfrgra  25011  isgrpo  25198  vci  25441  chnlei  26403  h1de2ctlem  26473  cmcmlem  26509  cmcm2i  26511  cmbr2i  26514  osumcor2i  26562  pjss2i  26598  ho01i  26747  nmop0h  26910  pjclem1  27114  jplem1  27187  atabs2i  27321  rabid2f  27400  preqsnd  27418  dfrel4  27454  subfacp1lem6  28629  mppspstlem  28931  quad3  29024  trpredmintr  29314  brdomain  29583  brrange  29584  brimg  29587  brapply  29588  brsuccf  29591  brfullfun  29598  brrestrict  29599  bpoly2  29819  bpoly3  29820  bpoly4  29821  rankeq1o  29828  ismblfin  30055  opropabco  30214  fdc  30238  isdrngo1  30359  smprngopr  30449  mzpcompact2lem  30684  eldioph4b  30745  2nn0ind  30881  islmodfg  31015  elnev  31345  dvnprodlem1  31743  fourierdlem103  31992  fourierdlem104  31993  usgra2pthlem1  32353  usgedgvadf1lem1  32413  usgedgvadf1lem2  32414  usgedgvadf1ALTlem1  32416  usgedgvadf1ALTlem2  32417  lindsrng01  33069  ldepspr  33074  bnj168  33785  bnj927  33827  bnj543  33951  bnj970  34005  bj-snsetex  34521  bj-pinftynminfty  34630  cdleme25cv  36084  cdlemk35  36638  dicval2  36906  dicopelval2  36908  dicelval2N  36909  hdmap1fval  37524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator