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

Theorem eqeq1i 2442
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 2441 . 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 1652
This theorem is referenced by:  ssequn2  3512  dfss1  3537  dfss4  3567  disj  3660  disjr  3661  undisj1  3671  undisj2  3672  undif  3700  uneqdifeq  3708  reusn  3869  rabsneu  3871  eusn  3872  tppreqb  3931  uniintsn  4079  iin0  4365  opeqsn  4444  dfepfr  4559  epfrc  4560  unisuc  4649  dmopab3  5073  dm0rn0  5077  ssdmres  5159  imadisj  5214  args  5223  dffr3  5227  intirr  5243  dminxp  5302  dfrel3  5319  fntpg  5497  fncnv  5506  dff1o4  5673  dffv4  5716  fvun2  5786  fnreseql  5831  fnotovb  6108  ovid  6181  ov  6184  ovg  6203  opiota  6526  tz7.49c  6694  sucprcreg  7556  inf3lem2  7573  zfregs2  7658  rankxpsuc  7795  scott0s  7801  cplem1  7802  cfslb2n  8137  fin23lem26  8194  dfacfin7  8268  axdc3lem4  8322  zorn2lem7  8371  alephom  8449  fpwwe2  8507  recmulnq  8830  recexsr  8971  map2psrpr  8974  renegcli  9351  elznn0  10285  xrsupss  10876  xrinfmss  10877  seqf1olem1  11350  seqf1olem2  11351  sqeqori  11481  hashprb  11656  hashbclem  11689  f1oun2prg  11852  oppgid  15140  lsmdisjr  15304  gexex  15456  dprd0  15577  oppr1  15727  opprunit  15754  opprdomn  16349  iinopn  16963  elcls  17125  ordthaus  17436  hauscmplem  17457  regr1lem2  17760  metdseq0  18872  minveclem1  19313  minveclem3b  19317  volun  19427  dyaddisj  19476  vieta1  20217  logeftb  20466  birthdaylem1  20778  lgseisenlem1  21121  rpvmasum  21208  usgraedgprv  21384  wlkdvspthlem  21595  rngosn3  22002  nmlno0lem  22282  minvecolem1  22364  hvsubeq0i  22553  hvsubaddi  22556  pjoc2i  22928  pjoml3i  23076  cmbr3i  23090  pjss2i  23170  hosubeq0i  23317  dmadjrnb  23397  nmlnop0iALT  23486  nmopcoadj0i  23594  stm1ri  23735  jplem2  23760  atoml2i  23874  chirredlem1  23881  cdj3lem3  23929  disjpreima  24014  mptfnf  24061  addeq0  24102  zrhchr  24348  braew  24581  aean  24583  ballotlemfp1  24737  dmgmaddn0  24795  cvmsss2  24949  cvmlift2lem13  24990  elrn3  25375  br1steq  25385  br2ndeq  25386  sspred  25429  dffr4  25437  tz6.26  25460  wfi  25462  frind  25498  wfrlem8  25518  sltsolem1  25577  axsegconlem6  25809  rankeq1o  26060  hfun  26067  totbndbnd  26435  coeq0  26747  fnresfnco  27904  afvpcfv0  27924  aovpcov0  27968  aov0ov0  27971  aovov0bi  27974  fnotaovb  27976  swrdccat3a  28105  shwrdssizesame  28171  1to3vfriswmgra  28255  frgrawopreg2  28298  zfregs2VD  28807  bnj1143  29015  atbase  29926  llnbase  30145  lplnbase  30170  lvolbase  30214  lhpbase  30634  cdlemg31b0N  31330  cdlemg31b0a  31331  cdlemh  31453
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator