Theorem eqeq1i 2745

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

Syntax hints:   ↔ wb 206   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqeq12i  2758  eqabb  2884  neeq1i  3011  dfss2  3994  ssequn2  4212  ineqcom  4231  sseqin2  4244  dfss7  4270  dfss4  4288  rabeq0w  4410  rabeq0  4411  disj  4473  disjr  4474  undisj1  4485  undisj2  4486  undif  4505  undifr  4506  undifrOLD  4507  uneqdifeq  4516  rabeqsn  4689  reusn  4752  rabsneu  4754  eusn  4755  tppreqb  4830  elpreqpr  4891  uniintsn  5009  iin0  5380  dfepfr  5684  epfrc  5685  dmopab3  5944  dm0rn0  5949  ssdmres  6042  iresn0n0  6083  imadisj  6109  args  6122  dffr3  6129  intirr  6150  dminxp  6211  dfrel3  6229  coeq0  6286  snres0  6329  sspred  6341  dffr4  6352  frpomin2  6373  frpoind  6374  tz6.26OLD  6380  wfiOLD  6383  cbviotavw  6533  fntpg  6638  fncnv  6651  mptfnf  6715  sbcfng  6744  f0rn0  6806  dff1o4  6870  dffv4  6917  tz6.12c  6942  fvun2  7014  fnreseql  7081  funopdmsn  7184  riota1  7426  riota2df  7428  riotaeqimp  7431  fnbrovb  7499  ovid  7591  ov  7594  ovg  7615  ovima0  7629  opiota  8100  frrlem13  8339  wfrlem8OLD  8372  tz7.49c  8502  sucprcreg  9670  zfregfr  9674  inf3lem2  9698  zfregs2  9802  frind  9819  rankxpsuc  9951  scott0s  9957  cplem1  9958  cfslb2n  10337  fin23lem26  10394  dfacfin7  10468  axdc3lem4  10522  zorn2lem7  10571  alephom  10654  fpwwe2  10712  recmulnq  11033  recexsr  11176  map2psrpr  11179  renegcli  11597  addeq0  11713  elznn0  12654  xrsupss  13371  xrinfmss  13372  prinfzo0  13755  seqf1olem1  14092  seqf1olem2  14093  sqeqori  14263  hashrabsn1  14423  hashprb  14446  hashprdifel  14447  hashbclem  14501  hash2pwpr  14525  f1oun2prg  14966  modfsummods  15841  cshwrepswhash1  17150  ismgmid  18703  smndex2dnrinv  18950  oppgid  19399  lsmdisjr  19726  gexex  19895  gsumxp2  20022  dprd0  20075  oppr1  20376  opprunit  20403  zringndrg  21502  gsummoncoe1  22333  mat0dimcrng  22497  iinopn  22929  elcls  23102  ordthaus  23413  hauscmplem  23435  regr1lem2  23769  metdseq0  24895  minveclem1  25477  minveclem3b  25481  volun  25599  dyaddisj  25650  vieta1  26372  logeftb  26643  birthdaylem1  27012  dmgmaddn0  27084  gausslemma2d  27436  lgseisenlem1  27437  2lgslem4  27468  rpvmasum  27588  sltsolem1  27738  noinfbnd2lem1  27793  madeval2  27910  made0  27930  axsegconlem6  28955  edg0iedg0  29090  numedglnl  29179  ushgredgedg  29264  ushgredgedgloop  29266  uhgr0v0e  29273  usgr1v0edg  29292  usgrexmpllem  29295  usgr1v0e  29361  nbuhgr2vtx1edgblem  29386  uvtx01vtx  29432  prcliscplgr  29449  cusgr0v  29463  vtxdg0e  29510  1loopgrvd2  29539  finsumvtxdg2ssteplem4  29584  finsumvtxdg2size  29586  isrgr  29595  fusgrregdegfi  29605  wspn0  29957  2wlkdlem8  29966  3wlkdlem8  30199  uhgr3cyclexlem  30213  1to2vfriswmgr  30311  1to3vfriswmgr  30312  frgrregorufr0  30356  frgrreg  30426  frgrregord013  30427  ex-ceil  30480  nmlno0lem  30825  minvecolem1  30906  hvsubeq0i  31095  hvsubaddi  31098  pjoc2i  31470  pjoml3i  31618  cmbr3i  31632  pjss2i  31712  hosubeq0i  31858  dmadjrnb  31938  nmlnop0iALT  32027  nmopcoadj0i  32135  stm1ri  32276  jplem2  32301  atoml2i  32415  chirredlem1  32422  cdj3lem3  32470  difininv  32547  disjnf  32592  disjpreima  32606  disjunsn  32616  f1od2  32735  wrdt2ind  32920  isunit2  33220  isdrng4  33264  lsmsnorb2  33385  ssdifidlprm  33451  zrhchr  33922  ddemeas  34200  braew  34206  aean  34208  eulerpartlemgh  34343  ballotlemfp1  34456  repr0  34588  hgt750lem2  34629  bnj1143  34766  nummin  35067  acycgr0v  35116  prclisacycgr  35119  cvmsss2  35242  cvmlift2lem13  35283  elrn3  35724  rankeq1o  36135  hfun  36142  bj-disj2r  36994  bj-sscon  36995  bj-0int  37067  bj-imdirco  37156  bj-pinftynminfty  37193  finxpreclem4  37360  nlpineqsn  37374  curunc  37562  tan2h  37572  poimirlem13  37593  poimirlem14  37594  poimirlem21  37601  poimirlem22  37602  asindmre  37663  totbndbnd  37749  rngosn3  37884  scott0f  38129  n0el2  38289  dfrel5  38302  dfrel6  38303  redundeq1  38585  dmqscoelseq  38617  dfeldisj5  38677  atbase  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  lhpbase  39955  cdlemg31b0N  40651  cdlemg31b0a  40652  cdlemh  40774  sticksstones16  42119  sticksstones21  42124  unitscyglem3  42154  metakunt24  42185  onsupmaxb  43200  iunrelexp0  43664  frege120  43945  clsk1indlem4  44006  gneispace  44096  scotteld  44215  undisjrab  44275  zfregs2VD  44812  dvnprod  45870  fnresfnco  46956  aiotavb  47005  afvpcfv0  47061  aovpcov0  47105  aov0ov0  47108  aovov0bi  47111  fnotaovb  47113  funressndmafv2rn  47138  fmtnoprmfac1lem  47438  lighneallem2  47480  snlindsntor  48200  rrx2pnedifcoorneorr  48451  itschlc0xyqsol1  48500  2itscp  48515  opndisj  48582