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

Theorem eqeq1i 2290
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 2289 . 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 1623
This theorem is referenced by:  ssequn2  3348  dfss1  3373  dfss4  3403  disj  3495  disjr  3496  undisj1  3506  undisj2  3507  undif  3534  uneqdifeq  3542  reusn  3700  rabsneu  3702  eusn  3703  uniintsn  3899  iin0  4184  opeqsn  4262  dfepfr  4378  epfrc  4379  unisuc  4468  dmopab3  4891  dm0rn0  4895  ssdmres  4977  imadisj  5032  args  5041  dffr3  5045  intirr  5061  dminxp  5118  dfrel3  5131  fncnv  5314  dff1o4  5480  dffv4  5522  fvun2  5591  fnreseql  5635  fnotovb  5894  ovid  5964  ov  5967  ovg  5986  opiota  6290  tz7.49c  6458  sucprcreg  7313  inf3lem2  7330  zfregs2  7415  rankxpsuc  7552  scott0s  7558  cplem1  7559  cfslb2n  7894  fin23lem26  7951  dfacfin7  8025  axdc3lem4  8079  zorn2lem7  8129  alephom  8207  fpwwe2  8265  recmulnq  8588  recexsr  8729  map2psrpr  8732  renegcli  9108  elznn0  10038  xrsupss  10627  xrinfmss  10628  seqf1olem1  11085  seqf1olem2  11086  sqeqori  11215  hashbclem  11390  oppgid  14829  lsmdisjr  14993  gexex  15145  dprd0  15266  oppr1  15416  opprunit  15443  opprdomn  16042  iinopn  16648  elcls  16810  ordthaus  17112  hauscmplem  17133  regr1lem2  17431  metdseq0  18358  minveclem1  18788  minveclem3b  18792  volun  18902  dyaddisj  18951  vieta1  19692  logeftb  19937  birthdaylem1  20246  lgseisenlem1  20588  rpvmasum  20675  rngosn3  21093  nmlno0lem  21371  minvecolem1  21453  hvsubeq0i  21642  hvsubaddi  21645  pjoc2i  22017  pjoml3i  22165  cmbr3i  22179  pjss2i  22259  hosubeq0i  22406  dmadjrnb  22486  nmlnop0iALT  22575  nmopcoadj0i  22683  stm1ri  22824  jplem2  22849  atoml2i  22963  chirredlem1  22970  cdj3lem3  23018  addeq0  23043  ballotlemfp1  23050  ballotlemfmpn  23053  mptfnf  23226  xrge0iifcnv  23315  disjpreima  23361  gsumconstf  23381  measvuni  23542  totprobd  23629  probmeasb  23633  dmgmaddn0  23695  cvmsss2  23805  cvmlift2lem13  23846  elrn3  24120  br1steq  24130  br2ndeq  24131  sspred  24174  dffr4  24182  tz6.26  24205  wfi  24207  frind  24243  wfrlem8  24263  sltsolem1  24322  axsegconlem6  24550  rankeq1o  24801  hfun  24808  clfsebsr  25349  trooo  25394  trinv  25395  vecval3b  25452  vecax3  25455  svli2  25484  dualded  25783  dualcat2  25784  homib  25796  nbssntrs  26147  totbndbnd  26513  coeq0  26831  fnresfnco  27989  afvpcfv0  28009  aovpcov0  28050  aov0ov0  28053  aovov0bi  28056  fnotaovb  28058  f1oun2prg  28076  usgraedgprv  28122  1to3vfriswmgra  28185  zfregs2VD  28617  bnj1143  28822  atbase  29479  llnbase  29698  lplnbase  29723  lvolbase  29767  lhpbase  30187  cdlemg31b0N  30883  cdlemg31b0a  30884  cdlemh  31006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator