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

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

Proof of Theorem eqeq1i
StepHypRef Expression
1 eqeq1i.1 . 2  |-  A  =  B
2 eqeq1 2393 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
31, 2ax-mp 8 1  |-  ( A  =  C  <->  B  =  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649
This theorem is referenced by:  ssequn2  3463  dfss1  3488  dfss4  3518  disj  3611  disjr  3612  undisj1  3622  undisj2  3623  undif  3651  uneqdifeq  3659  reusn  3820  rabsneu  3822  eusn  3823  tppreqb  3882  uniintsn  4029  iin0  4314  opeqsn  4393  dfepfr  4508  epfrc  4509  unisuc  4598  dmopab3  5022  dm0rn0  5026  ssdmres  5108  imadisj  5163  args  5172  dffr3  5176  intirr  5192  dminxp  5251  dfrel3  5268  fntpg  5446  fncnv  5455  dff1o4  5622  dffv4  5665  fvun2  5734  fnreseql  5779  fnotovb  6056  ovid  6129  ov  6132  ovg  6151  opiota  6471  tz7.49c  6639  sucprcreg  7500  inf3lem2  7517  zfregs2  7602  rankxpsuc  7739  scott0s  7745  cplem1  7746  cfslb2n  8081  fin23lem26  8138  dfacfin7  8212  axdc3lem4  8266  zorn2lem7  8315  alephom  8393  fpwwe2  8451  recmulnq  8774  recexsr  8915  map2psrpr  8918  renegcli  9294  elznn0  10228  xrsupss  10819  xrinfmss  10820  seqf1olem1  11289  seqf1olem2  11290  sqeqori  11420  hashprb  11595  hashbclem  11628  f1oun2prg  11791  oppgid  15079  lsmdisjr  15243  gexex  15395  dprd0  15516  oppr1  15666  opprunit  15693  opprdomn  16288  iinopn  16898  elcls  17060  ordthaus  17370  hauscmplem  17391  regr1lem2  17693  metdseq0  18755  minveclem1  19192  minveclem3b  19196  volun  19306  dyaddisj  19355  vieta1  20096  logeftb  20345  birthdaylem1  20657  lgseisenlem1  21000  rpvmasum  21087  usgraedgprv  21263  wlkdvspthlem  21455  rngosn3  21862  nmlno0lem  22142  minvecolem1  22224  hvsubeq0i  22413  hvsubaddi  22416  pjoc2i  22788  pjoml3i  22936  cmbr3i  22950  pjss2i  23030  hosubeq0i  23177  dmadjrnb  23257  nmlnop0iALT  23346  nmopcoadj0i  23454  stm1ri  23595  jplem2  23620  atoml2i  23734  chirredlem1  23741  cdj3lem3  23789  disjpreima  23870  mptfnf  23915  addeq0  23955  zrhchr  24159  braew  24387  aean  24389  ballotlemfp1  24528  dmgmaddn0  24586  cvmsss2  24740  cvmlift2lem13  24781  elrn3  25144  br1steq  25154  br2ndeq  25155  sspred  25198  dffr4  25206  tz6.26  25229  wfi  25231  frind  25267  wfrlem8  25287  sltsolem1  25346  axsegconlem6  25575  rankeq1o  25826  hfun  25833  totbndbnd  26189  coeq0  26501  fnresfnco  27659  afvpcfv0  27679  aovpcov0  27723  aov0ov0  27726  aovov0bi  27729  fnotaovb  27731  1to3vfriswmgra  27760  frgrawopreg2  27803  zfregs2VD  28294  bnj1143  28499  atbase  29404  llnbase  29623  lplnbase  29648  lvolbase  29692  lhpbase  30112  cdlemg31b0N  30808  cdlemg31b0a  30809  cdlemh  30931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380
  Copyright terms: Public domain W3C validator