Theorem eqeq1i 2742

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

Hypothesis

Ref	Expression
eqeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq1i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq1 2741	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  eqeq12i  2755  eqabb  2881  neeq1i  3005  dfss2  3969  ssequn2  4189  ineqcom  4210  sseqin2  4223  dfss7  4251  dfss4  4269  rabeq0w  4387  rabeq0  4388  disj  4450  disjr  4451  undisj1  4462  undisj2  4463  undif  4482  undifr  4483  undifrOLD  4484  uneqdifeq  4493  rabeqsn  4667  reusn  4727  rabsneu  4729  eusn  4730  tppreqb  4805  elpreqpr  4867  uniintsn  4985  iin0  5362  dfepfr  5669  epfrc  5670  dmopab3  5930  dm0rn0  5935  rnopab3  5967  ssdmres  6031  iresn0n0  6072  imadisj  6098  args  6110  dffr3  6117  intirr  6138  dminxp  6200  dfrel3  6218  coeq0  6275  snres0  6318  sspred  6330  dffr4  6341  frpomin2  6362  frpoind  6363  tz6.26OLD  6369  wfiOLD  6372  cbviotavw  6522  fntpg  6626  fncnv  6639  mptfnf  6703  sbcfng  6733  f0rn0  6793  dff1o4  6856  dffv4  6903  tz6.12c  6928  fvun2  7001  fnreseql  7068  funopdmsn  7170  riota1  7409  riota2df  7411  riotaeqimp  7414  fnbrovb  7482  ovid  7574  ov  7577  ovg  7598  ovima0  7612  opiota  8084  frrlem13  8323  wfrlem8OLD  8356  tz7.49c  8486  sucprcreg  9641  zfregfr  9645  inf3lem2  9669  zfregs2  9773  frind  9790  rankxpsuc  9922  scott0s  9928  cplem1  9929  cfslb2n  10308  fin23lem26  10365  dfacfin7  10439  axdc3lem4  10493  zorn2lem7  10542  alephom  10625  fpwwe2  10683  recmulnq  11004  recexsr  11147  map2psrpr  11150  renegcli  11570  addeq0  11686  elznn0  12628  xrsupss  13351  xrinfmss  13352  prinfzo0  13738  seqf1olem1  14082  seqf1olem2  14083  sqeqori  14253  hashrabsn1  14413  hashprb  14436  hashprdifel  14437  hashbclem  14491  hash2pwpr  14515  f1oun2prg  14956  modfsummods  15829  cshwrepswhash1  17140  ismgmid  18678  smndex2dnrinv  18928  oppgid  19375  lsmdisjr  19702  gexex  19871  gsumxp2  19998  dprd0  20051  oppr1  20350  opprunit  20377  zringndrg  21479  gsummoncoe1  22312  mat0dimcrng  22476  iinopn  22908  elcls  23081  ordthaus  23392  hauscmplem  23414  regr1lem2  23748  metdseq0  24876  minveclem1  25458  minveclem3b  25462  volun  25580  dyaddisj  25631  vieta1  26354  logeftb  26625  birthdaylem1  26994  dmgmaddn0  27066  gausslemma2d  27418  lgseisenlem1  27419  2lgslem4  27450  rpvmasum  27570  sltsolem1  27720  noinfbnd2lem1  27775  madeval2  27892  made0  27912  axsegconlem6  28937  edg0iedg0  29072  numedglnl  29161  ushgredgedg  29246  ushgredgedgloop  29248  uhgr0v0e  29255  usgr1v0edg  29274  usgrexmpllem  29277  usgr1v0e  29343  nbuhgr2vtx1edgblem  29368  uvtx01vtx  29414  prcliscplgr  29431  cusgr0v  29445  vtxdg0e  29492  1loopgrvd2  29521  finsumvtxdg2ssteplem4  29566  finsumvtxdg2size  29568  isrgr  29577  fusgrregdegfi  29587  wspn0  29944  2wlkdlem8  29953  3wlkdlem8  30186  uhgr3cyclexlem  30200  1to2vfriswmgr  30298  1to3vfriswmgr  30299  frgrregorufr0  30343  frgrreg  30413  frgrregord013  30414  ex-ceil  30467  nmlno0lem  30812  minvecolem1  30893  hvsubeq0i  31082  hvsubaddi  31085  pjoc2i  31457  pjoml3i  31605  cmbr3i  31619  pjss2i  31699  hosubeq0i  31845  dmadjrnb  31925  nmlnop0iALT  32014  nmopcoadj0i  32122  stm1ri  32263  jplem2  32288  atoml2i  32402  chirredlem1  32409  cdj3lem3  32457  difininv  32536  disjnf  32583  disjpreima  32597  disjunsn  32607  f1od2  32732  wrdt2ind  32938  isunit2  33244  isdrng4  33298  lsmsnorb2  33420  ssdifidlprm  33486  fldext2chn  33769  zrhchr  33975  ddemeas  34237  braew  34243  aean  34245  eulerpartlemgh  34380  ballotlemfp1  34494  repr0  34626  hgt750lem2  34667  bnj1143  34804  nummin  35105  acycgr0v  35153  prclisacycgr  35156  cvmsss2  35279  cvmlift2lem13  35320  elrn3  35762  rankeq1o  36172  hfun  36179  bj-disj2r  37029  bj-sscon  37030  bj-0int  37102  bj-imdirco  37191  bj-pinftynminfty  37228  finxpreclem4  37395  nlpineqsn  37409  curunc  37609  tan2h  37619  poimirlem13  37640  poimirlem14  37641  poimirlem21  37648  poimirlem22  37649  asindmre  37710  totbndbnd  37796  rngosn3  37931  scott0f  38176  n0el2  38334  dfrel5  38347  dfrel6  38348  redundeq1  38630  dmqscoelseq  38662  dfeldisj5  38722  atbase  39290  llnbase  39511  lplnbase  39536  lvolbase  39580  lhpbase  40000  cdlemg31b0N  40696  cdlemg31b0a  40697  cdlemh  40819  sticksstones16  42163  sticksstones21  42168  unitscyglem3  42198  metakunt24  42229  onsupmaxb  43251  iunrelexp0  43715  frege120  43996  clsk1indlem4  44057  gneispace  44147  scotteld  44265  undisjrab  44325  zfregs2VD  44861  dvnprod  45964  fnresfnco  47053  aiotavb  47102  afvpcfv0  47158  aovpcov0  47202  aov0ov0  47205  aovov0bi  47208  fnotaovb  47210  funressndmafv2rn  47235  fmtnoprmfac1lem  47551  lighneallem2  47593  stgrvtx0  47929  isubgr3stgrlem6  47938  snlindsntor  48388  rrx2pnedifcoorneorr  48638  itschlc0xyqsol1  48687  2itscp  48702  resinsn  48772  resinsnALT  48773  opndisj  48800  istermc  49121