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

Theorem eqeq1i 2449
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 2448 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
31, 2ax-mp 5 1  |-  ( A  =  C  <->  B  =  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653
This theorem is referenced by:  ssequn2  3506  dfss1  3531  dfss4  3560  disj  3692  disjr  3693  undisj1  3703  undisj2  3704  undif  3732  uneqdifeq  3740  reusn  3901  rabsneu  3903  eusn  3904  tppreqb  3963  uniintsn  4111  iin0  4402  opeqsn  4481  dfepfr  4596  epfrc  4597  unisuc  4686  dmopab3  5111  dm0rn0  5115  ssdmres  5197  imadisj  5252  args  5261  dffr3  5265  intirr  5281  dminxp  5340  dfrel3  5357  fntpg  5535  fncnv  5544  dff1o4  5711  dffv4  5754  fvun2  5824  fnreseql  5869  fnotovb  6146  ovid  6219  ov  6222  ovg  6241  opiota  6564  tz7.49c  6732  sucprcreg  7596  inf3lem2  7613  zfregs2  7698  rankxpsuc  7837  scott0s  7843  cplem1  7844  cfslb2n  8179  fin23lem26  8236  dfacfin7  8310  axdc3lem4  8364  zorn2lem7  8413  alephom  8491  fpwwe2  8549  recmulnq  8872  recexsr  9013  map2psrpr  9016  renegcli  9393  elznn0  10327  xrsupss  10918  xrinfmss  10919  seqf1olem1  11393  seqf1olem2  11394  sqeqori  11524  hashprb  11699  hashbclem  11732  f1oun2prg  11895  oppgid  15183  lsmdisjr  15347  gexex  15499  dprd0  15620  oppr1  15770  opprunit  15797  opprdomn  16392  iinopn  17006  elcls  17168  ordthaus  17479  hauscmplem  17500  regr1lem2  17803  metdseq0  18915  minveclem1  19356  minveclem3b  19360  volun  19470  dyaddisj  19519  vieta1  20260  logeftb  20509  birthdaylem1  20821  lgseisenlem1  21164  rpvmasum  21251  usgraedgprv  21427  wlkdvspthlem  21638  rngosn3  22045  nmlno0lem  22325  minvecolem1  22407  hvsubeq0i  22596  hvsubaddi  22599  pjoc2i  22971  pjoml3i  23119  cmbr3i  23133  pjss2i  23213  hosubeq0i  23360  dmadjrnb  23440  nmlnop0iALT  23529  nmopcoadj0i  23637  stm1ri  23778  jplem2  23803  atoml2i  23917  chirredlem1  23924  cdj3lem3  23972  disjpreima  24057  mptfnf  24104  addeq0  24145  zrhchr  24391  braew  24624  aean  24626  ballotlemfp1  24780  dmgmaddn0  24838  cvmsss2  24992  cvmlift2lem13  25033  elrn3  25417  br1steq  25429  br2ndeq  25430  sspred  25478  dffr4  25488  tz6.26  25511  wfi  25513  frind  25549  wfrlem8  25576  sltsolem1  25654  axsegconlem6  25892  rankeq1o  26143  hfun  26150  tan2h  26276  totbndbnd  26536  coeq0  26848  fnresfnco  28004  afvpcfv0  28024  aovpcov0  28068  aov0ov0  28071  aovov0bi  28074  fnotaovb  28076  f0rn0  28117  swrdccat3a  28275  cshwssizesame  28346  1to3vfriswmgra  28495  frgrawopreg2  28538  zfregs2VD  29051  bnj1143  29259  atbase  30185  llnbase  30404  lplnbase  30429  lvolbase  30473  lhpbase  30893  cdlemg31b0N  31589  cdlemg31b0a  31590  cdlemh  31712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2435
  Copyright terms: Public domain W3C validator