Theorem eqeq1i 2730

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 2729	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  eqeq12i  2743  eqabb  2865  neeq1i  2994  dfss2  3962  ssequn2  4181  ineqcom  4200  sseqin2  4213  dfss7  4239  dfss4  4257  rabeq0w  4385  rabeq0  4386  disj  4449  disjOLD  4450  disjr  4451  undisj1  4463  undisj2  4464  undif  4483  undifr  4484  undifrOLD  4485  uneqdifeq  4494  rabeqsn  4671  reusn  4733  rabsneu  4735  eusn  4736  tppreqb  4810  elpreqpr  4869  uniintsn  4991  iin0  5362  dfepfr  5663  epfrc  5664  dmopab3  5922  dm0rn0  5927  ssdmres  6018  iresn0n0  6058  imadisj  6084  args  6097  dffr3  6104  intirr  6125  dminxp  6186  dfrel3  6204  coeq0  6261  snres0  6304  sspred  6316  dffr4  6327  frpomin2  6349  frpoind  6350  tz6.26OLD  6356  wfiOLD  6359  cbviotavw  6509  fntpg  6614  fncnv  6627  mptfnf  6691  sbcfng  6720  f0rn0  6782  dff1o4  6846  dffv4  6893  tz6.12c  6918  fvun2  6989  fnreseql  7056  funopdmsn  7159  riota1  7397  riota2df  7399  riotaeqimp  7402  fnbrovb  7469  ovid  7562  ov  7565  ovg  7586  ovima0  7600  opiota  8064  frrlem13  8304  wfrlem8OLD  8337  tz7.49c  8467  sucprcreg  9626  zfregfr  9630  inf3lem2  9654  zfregs2  9758  frind  9775  rankxpsuc  9907  scott0s  9913  cplem1  9914  cfslb2n  10293  fin23lem26  10350  dfacfin7  10424  axdc3lem4  10478  zorn2lem7  10527  alephom  10610  fpwwe2  10668  recmulnq  10989  recexsr  11132  map2psrpr  11135  renegcli  11553  addeq0  11669  elznn0  12606  xrsupss  13323  xrinfmss  13324  prinfzo0  13706  seqf1olem1  14042  seqf1olem2  14043  sqeqori  14213  hashrabsn1  14369  hashprb  14392  hashprdifel  14393  hashbclem  14447  hash2pwpr  14473  f1oun2prg  14904  modfsummods  15775  cshwrepswhash1  17075  ismgmid  18628  smndex2dnrinv  18875  oppgid  19322  lsmdisjr  19651  gexex  19820  gsumxp2  19947  dprd0  20000  oppr1  20301  opprunit  20328  opprdomn  21268  zringndrg  21411  gsummoncoe1  22252  mat0dimcrng  22416  iinopn  22848  elcls  23021  ordthaus  23332  hauscmplem  23354  regr1lem2  23688  metdseq0  24814  minveclem1  25396  minveclem3b  25400  volun  25518  dyaddisj  25569  vieta1  26292  logeftb  26562  birthdaylem1  26928  dmgmaddn0  27000  gausslemma2d  27352  lgseisenlem1  27353  2lgslem4  27384  rpvmasum  27504  sltsolem1  27654  noinfbnd2lem1  27709  madeval2  27826  made0  27846  axsegconlem6  28805  edg0iedg0  28940  numedglnl  29029  ushgredgedg  29114  ushgredgedgloop  29116  uhgr0v0e  29123  usgr1v0edg  29142  usgrexmpllem  29145  usgr1v0e  29211  nbuhgr2vtx1edgblem  29236  uvtx01vtx  29282  prcliscplgr  29299  cusgr0v  29313  vtxdg0e  29360  1loopgrvd2  29389  finsumvtxdg2ssteplem4  29434  finsumvtxdg2size  29436  isrgr  29445  fusgrregdegfi  29455  wspn0  29807  2wlkdlem8  29816  3wlkdlem8  30049  uhgr3cyclexlem  30063  1to2vfriswmgr  30161  1to3vfriswmgr  30162  frgrregorufr0  30206  frgrreg  30276  frgrregord013  30277  ex-ceil  30330  nmlno0lem  30675  minvecolem1  30756  hvsubeq0i  30945  hvsubaddi  30948  pjoc2i  31320  pjoml3i  31468  cmbr3i  31482  pjss2i  31562  hosubeq0i  31708  dmadjrnb  31788  nmlnop0iALT  31877  nmopcoadj0i  31985  stm1ri  32126  jplem2  32151  atoml2i  32265  chirredlem1  32272  cdj3lem3  32320  difininv  32392  disjnf  32439  disjpreima  32453  disjunsn  32463  f1od2  32585  wrdt2ind  32763  isdrng4  33083  lsmsnorb2  33204  ssdifidlprm  33270  zrhchr  33708  ddemeas  33986  braew  33992  aean  33994  eulerpartlemgh  34129  ballotlemfp1  34242  repr0  34374  hgt750lem2  34415  bnj1143  34552  nummin  34845  acycgr0v  34889  prclisacycgr  34892  cvmsss2  35015  cvmlift2lem13  35056  elrn3  35487  rankeq1o  35898  hfun  35905  bj-disj2r  36638  bj-sscon  36639  bj-0int  36711  bj-imdirco  36800  bj-pinftynminfty  36837  finxpreclem4  37004  nlpineqsn  37018  curunc  37206  tan2h  37216  poimirlem13  37237  poimirlem14  37238  poimirlem21  37245  poimirlem22  37246  asindmre  37307  totbndbnd  37393  rngosn3  37528  scott0f  37773  n0el2  37935  dfrel5  37948  dfrel6  37949  redundeq1  38231  dmqscoelseq  38263  dfeldisj5  38323  atbase  38891  llnbase  39112  lplnbase  39137  lvolbase  39181  lhpbase  39601  cdlemg31b0N  40297  cdlemg31b0a  40298  cdlemh  40420  sticksstones16  41765  sticksstones21  41770  metakunt24  41814  onsupmaxb  42809  iunrelexp0  43274  frege120  43555  clsk1indlem4  43616  gneispace  43706  scotteld  43825  undisjrab  43885  zfregs2VD  44422  dvnprod  45475  fnresfnco  46561  aiotavb  46608  afvpcfv0  46664  aovpcov0  46708  aov0ov0  46711  aovov0bi  46714  fnotaovb  46716  funressndmafv2rn  46741  fmtnoprmfac1lem  47041  lighneallem2  47083  snlindsntor  47725  rrx2pnedifcoorneorr  47976  itschlc0xyqsol1  48025  2itscp  48040  opndisj  48107