Theorem eqeq1i 2627

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	|- A = B

Assertion

Ref	Expression
eqeq1i	|- ( A = C <-> B = C )

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 |- A = B
2		eqeq1 2626	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 5	1 |- ( A = C <-> B = C )

Syntax hints:   <-> wb 196   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqeq12i  2636  neeq1i  2858  ssequn2  3786  sseqin2  3817  dfss1OLD  3818  dfss4  3858  rabeq0  3957  disj  4017  disjr  4018  undisj1  4029  undisj2  4030  undif  4049  uneqdifeq  4057  uneqdifeqOLD  4058  reusn  4262  rabsneu  4264  eusn  4265  tppreqb  4336  elpreqpr  4396  uniintsn  4514  iin0  4839  opeqsn  4967  dfepfr  5099  epfrc  5100  dmopab3  5337  dm0rn0  5342  ssdmres  5420  imadisj  5484  args  5493  dffr3  5498  intirr  5514  dminxp  5574  dfrel3  5592  coeq0  5644  sspred  5688  dffr4  5696  tz6.26  5711  wfi  5713  unisuc  5801  fntpg  5948  fncnv  5962  mptfnf  6015  sbcfng  6042  f0rn0  6090  dff1o4  6145  dffv4  6188  fvun2  6270  fnreseql  6327  funopdmsn  6415  riota1  6629  riota2df  6631  riotaeqimp  6634  fnotovb  6694  ovid  6777  ov  6780  ovg  6799  ovima0  6813  opiota  7229  wfrlem8  7422  tz7.49c  7541  sucprcreg  8506  zfregfr  8509  inf3lem2  8526  zfregs2  8609  rankxpsuc  8745  scott0s  8751  cplem1  8752  cfslb2n  9090  fin23lem26  9147  dfacfin7  9221  axdc3lem4  9275  zorn2lem7  9324  alephom  9407  fpwwe2  9465  recmulnq  9786  recexsr  9928  map2psrpr  9931  renegcli  10342  elznn0  11392  xrsupss  12139  xrinfmss  12140  prinfzo0  12506  seqf1olem1  12840  seqf1olem2  12841  sqeqori  12976  hashrabsn1  13163  hashprb  13185  hashprdifel  13186  hashbclem  13236  hash2pwpr  13258  swrdccat3a  13494  f1oun2prg  13662  modfsummods  14525  cshwrepswhash1  15809  ismgmid  17264  oppgid  17786  lsmdisjr  18097  gexex  18256  dprd0  18430  oppr1  18634  opprunit  18661  opprdomn  19301  gsummoncoe1  19674  zringndrg  19838  mat0dimcrng  20276  iinopn  20707  elcls  20877  ordthaus  21188  hauscmplem  21209  regr1lem2  21543  metdseq0  22657  minveclem1  23195  minveclem3b  23199  volun  23313  dyaddisj  23364  vieta1  24067  logeftb  24330  birthdaylem1  24678  dmgmaddn0  24749  gausslemma2d  25099  lgseisenlem1  25100  2lgslem4  25131  rpvmasum  25215  axsegconlem6  25802  edg0iedg0  25949  numedglnl  26039  ushgredgedg  26121  ushgredgedgloop  26123  uhgr0v0e  26130  usgr1v0edg  26149  usgrexmpllem  26152  usgr1v0e  26218  nbuhgr2vtx1edgblem  26247  uvtxa01vtx0  26297  uvtxa01vtx  26298  cusgr0v  26324  vtxdg0e  26370  1loopgrvd2  26399  finsumvtxdg2ssteplem4  26444  finsumvtxdg2size  26446  isrgr  26455  fusgrregdegfi  26465  wlknwwlksnsur  26776  wlkwwlksur  26783  2wlkdlem8  26829  clwlksfclwwlk1hashn  26959  clwlksfoclwwlk  26963  3wlkdlem8  27027  uhgr3cyclexlem  27041  1to2vfriswmgr  27143  1to3vfriswmgr  27144  frgrregorufr0  27188  frgrreg  27252  frgrregord013  27253  ex-ceil  27305  nmlno0lem  27648  minvecolem1  27730  hvsubeq0i  27920  hvsubaddi  27923  pjoc2i  28297  pjoml3i  28445  cmbr3i  28459  pjss2i  28539  hosubeq0i  28685  dmadjrnb  28765  nmlnop0iALT  28854  nmopcoadj0i  28962  stm1ri  29103  jplem2  29128  atoml2i  29242  chirredlem1  29249  cdj3lem3  29297  difininv  29354  disjnf  29384  disjpreima  29397  disjunsn  29407  f1od2  29499  addeq0  29510  zrhchr  30020  ddemeas  30299  braew  30305  aean  30307  eulerpartlemgh  30440  ballotlemfp1  30553  repr0  30689  hgt750lem2  30730  bnj1143  30861  cvmsss2  31256  cvmlift2lem13  31297  elrn3  31652  br1steq  31670  br2ndeq  31671  frind  31740  sltsolem1  31826  madeval2  31936  rankeq1o  32278  hfun  32285  bj-disj2r  33013  bj-sscon  33014  bj-0int  33055  bj-pinftynminfty  33114  finxpreclem4  33231  curunc  33391  tan2h  33401  poimirlem13  33422  poimirlem14  33423  poimirlem21  33430  poimirlem22  33431  asindmre  33495  totbndbnd  33588  rngosn3  33723  scott0f  33977  ineqcom  34005  n0el2  34103  dfrel5  34114  dfrel6  34115  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  lhpbase  35284  cdlemg31b0N  35982  cdlemg31b0a  35983  cdlemh  36105  iunrelexp0  37994  frege120  38277  clsk1indlem4  38342  gneispace  38432  undisjrab  38505  zfregs2VD  39076  dvnprod  40164  fnresfnco  41206  afvpcfv0  41226  aovpcov0  41270  aov0ov0  41273  aovov0bi  41276  fnotaovb  41278  fmtnoprmfac1lem  41476  lighneallem2  41523  snlindsntor  42260