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

Theorem eqeq1i 2303
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 2302 . 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 176    = wceq 1632
This theorem is referenced by:  ssequn2  3361  dfss1  3386  dfss4  3416  disj  3508  disjr  3509  undisj1  3519  undisj2  3520  undif  3547  uneqdifeq  3555  reusn  3713  rabsneu  3715  eusn  3716  uniintsn  3915  iin0  4200  opeqsn  4278  dfepfr  4394  epfrc  4395  unisuc  4484  dmopab3  4907  dm0rn0  4911  ssdmres  4993  imadisj  5048  args  5057  dffr3  5061  intirr  5077  dminxp  5134  dfrel3  5147  fncnv  5330  dff1o4  5496  dffv4  5538  fvun2  5607  fnreseql  5651  fnotovb  5910  ovid  5980  ov  5983  ovg  6002  opiota  6306  tz7.49c  6474  sucprcreg  7329  inf3lem2  7346  zfregs2  7431  rankxpsuc  7568  scott0s  7574  cplem1  7575  cfslb2n  7910  fin23lem26  7967  dfacfin7  8041  axdc3lem4  8095  zorn2lem7  8145  alephom  8223  fpwwe2  8281  recmulnq  8604  recexsr  8745  map2psrpr  8748  renegcli  9124  elznn0  10054  xrsupss  10643  xrinfmss  10644  seqf1olem1  11101  seqf1olem2  11102  sqeqori  11231  hashbclem  11406  oppgid  14845  lsmdisjr  15009  gexex  15161  dprd0  15282  oppr1  15432  opprunit  15459  opprdomn  16058  iinopn  16664  elcls  16826  ordthaus  17128  hauscmplem  17149  regr1lem2  17447  metdseq0  18374  minveclem1  18804  minveclem3b  18808  volun  18918  dyaddisj  18967  vieta1  19708  logeftb  19953  birthdaylem1  20262  lgseisenlem1  20604  rpvmasum  20691  rngosn3  21109  nmlno0lem  21387  minvecolem1  21469  hvsubeq0i  21658  hvsubaddi  21661  pjoc2i  22033  pjoml3i  22181  cmbr3i  22195  pjss2i  22275  hosubeq0i  22422  dmadjrnb  22502  nmlnop0iALT  22591  nmopcoadj0i  22699  stm1ri  22840  jplem2  22865  atoml2i  22979  chirredlem1  22986  cdj3lem3  23034  addeq0  23059  ballotlemfp1  23066  ballotlemfmpn  23069  mptfnf  23241  xrge0iifcnv  23330  disjpreima  23376  gsumconstf  23396  measvuni  23557  totprobd  23644  probmeasb  23648  dmgmaddn0  23710  cvmsss2  23820  cvmlift2lem13  23861  elrn3  24191  br1steq  24201  br2ndeq  24202  sspred  24245  dffr4  24253  tz6.26  24276  wfi  24278  frind  24314  wfrlem8  24334  sltsolem1  24393  axsegconlem6  24622  rankeq1o  24873  hfun  24880  clfsebsr  25452  trooo  25497  trinv  25498  vecval3b  25555  vecax3  25558  svli2  25587  dualded  25886  dualcat2  25887  homib  25899  nbssntrs  26250  totbndbnd  26616  coeq0  26934  fnresfnco  28094  afvpcfv0  28114  aovpcov0  28158  aov0ov0  28161  aovov0bi  28164  fnotaovb  28166  f1oun2prg  28187  usgraedgprv  28256  wlkdvspthlem  28365  1to3vfriswmgra  28431  zfregs2VD  28933  bnj1143  29138  atbase  30101  llnbase  30320  lplnbase  30345  lvolbase  30389  lhpbase  30809  cdlemg31b0N  31505  cdlemg31b0a  31506  cdlemh  31628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator