Theorem eqeq1i 2736

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

Syntax hints:   ↔ wb 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqeq12i  2749  eqabb  2870  neeq1i  2992  dfss2  3915  ssequn2  4134  ineqcom  4155  sseqin2  4168  dfss7  4196  dfss4  4214  rabeq0w  4332  rabeq0  4333  disj  4395  disjr  4396  undisj1  4407  undisj2  4408  undif  4427  undifr  4428  undifrOLD  4429  uneqdifeq  4438  rabeqsn  4615  reusn  4675  rabsneu  4677  eusn  4678  tppreqb  4752  elpreqpr  4814  uniintsn  4930  iin0  5295  dfepfr  5595  epfrc  5596  dmopab3  5854  dm0rn0  5859  dm0rn0OLD  5860  rnopab3  5891  ssdmres  5957  iresn0n0  5998  imadisj  6024  args  6036  dffr3  6043  intirr  6060  dminxp  6122  dfrel3  6140  coeq0  6198  snres0  6240  sspred  6252  dffr4  6262  frpomin2  6283  frpoind  6284  cbviotavw  6440  fntpg  6536  fncnv  6549  mptfnf  6611  sbcfng  6643  f0rn0  6703  dff1o4  6766  dffv4  6814  tz6.12c  6839  fvun2  6909  fnreseql  6976  funopdmsn  7078  riota1  7319  riota2df  7321  riotaeqimp  7324  fnbrovb  7392  ovid  7482  ov  7485  ovg  7506  ovima0  7520  opiota  7986  frrlem13  8223  tz7.49c  8360  sucprcreg  9485  zfregfr  9489  inf3lem2  9514  zfregs2  9618  frind  9638  rankxpsuc  9770  scott0s  9776  cplem1  9777  cfslb2n  10154  fin23lem26  10211  dfacfin7  10285  axdc3lem4  10339  zorn2lem7  10388  alephom  10471  fpwwe2  10529  recmulnq  10850  recexsr  10993  map2psrpr  10996  renegcli  11417  addeq0  11535  elznn0  12478  xrsupss  13203  xrinfmss  13204  prinfzo0  13593  seqf1olem1  13943  seqf1olem2  13944  sqeqori  14116  hashrabsn1  14276  hashprb  14299  hashprdifel  14300  hashbclem  14354  hash2pwpr  14378  f1oun2prg  14819  modfsummods  15695  cshwrepswhash1  17009  ismgmid  18568  smndex2dnrinv  18818  oppgid  19263  lsmdisjr  19591  gexex  19760  gsumxp2  19887  dprd0  19940  oppr1  20263  opprunit  20290  zringndrg  21400  gsummoncoe1  22218  mat0dimcrng  22380  iinopn  22812  elcls  22983  ordthaus  23294  hauscmplem  23316  regr1lem2  23650  metdseq0  24765  minveclem1  25346  minveclem3b  25350  volun  25468  dyaddisj  25519  vieta1  26242  logeftb  26514  birthdaylem1  26883  dmgmaddn0  26955  gausslemma2d  27307  lgseisenlem1  27308  2lgslem4  27339  rpvmasum  27459  sltsolem1  27609  noinfbnd2lem1  27664  madeval2  27789  made0  27813  axsegconlem6  28895  edg0iedg0  29028  numedglnl  29117  ushgredgedg  29202  ushgredgedgloop  29204  uhgr0v0e  29211  usgr1v0edg  29230  usgrexmpllem  29233  usgr1v0e  29299  nbuhgr2vtx1edgblem  29324  uvtx01vtx  29370  prcliscplgr  29387  cusgr0v  29401  vtxdg0e  29448  1loopgrvd2  29477  finsumvtxdg2ssteplem4  29522  finsumvtxdg2size  29524  isrgr  29533  fusgrregdegfi  29543  wspn0  29897  2wlkdlem8  29906  3wlkdlem8  30139  uhgr3cyclexlem  30153  1to2vfriswmgr  30251  1to3vfriswmgr  30252  frgrregorufr0  30296  frgrreg  30366  frgrregord013  30367  ex-ceil  30420  nmlno0lem  30765  minvecolem1  30846  hvsubeq0i  31035  hvsubaddi  31038  pjoc2i  31410  pjoml3i  31558  cmbr3i  31572  pjss2i  31652  hosubeq0i  31798  dmadjrnb  31878  nmlnop0iALT  31967  nmopcoadj0i  32075  stm1ri  32216  jplem2  32241  atoml2i  32355  chirredlem1  32362  cdj3lem3  32410  difininv  32489  disjnf  32542  disjpreima  32556  disjunsn  32566  f1od2  32694  wrdt2ind  32926  isunit2  33199  isdrng4  33253  lsmsnorb2  33349  ssdifidlprm  33415  fldext2chn  33733  zrhchr  33979  ddemeas  34241  braew  34247  aean  34249  eulerpartlemgh  34383  ballotlemfp1  34497  repr0  34616  hgt750lem2  34657  bnj1143  34794  nummin  35096  acycgr0v  35184  prclisacycgr  35187  cvmsss2  35310  cvmlift2lem13  35351  elrn3  35798  rankeq1o  36205  hfun  36212  bj-disj2r  37062  bj-sscon  37063  bj-0int  37135  bj-imdirco  37224  bj-pinftynminfty  37261  finxpreclem4  37428  nlpineqsn  37442  curunc  37642  tan2h  37652  poimirlem13  37673  poimirlem14  37674  poimirlem21  37681  poimirlem22  37682  asindmre  37743  totbndbnd  37829  rngosn3  37964  scott0f  38209  n0el2  38363  dfrel5  38374  dfrel6  38375  redundeq1  38666  dmqscoelseq  38699  dfeldisj5  38759  atbase  39328  llnbase  39548  lplnbase  39573  lvolbase  39617  lhpbase  40037  cdlemg31b0N  40733  cdlemg31b0a  40734  cdlemh  40856  sticksstones16  42195  sticksstones21  42200  unitscyglem3  42230  onsupmaxb  43272  iunrelexp0  43735  frege120  44016  clsk1indlem4  44077  gneispace  44167  scotteld  44279  undisjrab  44339  zfregs2VD  44873  dvnprod  45987  fnresfnco  47072  aiotavb  47121  afvpcfv0  47177  aovpcov0  47221  aov0ov0  47224  aovov0bi  47227  fnotaovb  47229  funressndmafv2rn  47254  fmtnoprmfac1lem  47595  lighneallem2  47637  stgrvtx0  47993  isubgr3stgrlem6  48002  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  snlindsntor  48503  rrx2pnedifcoorneorr  48749  itschlc0xyqsol1  48798  2itscp  48813  resinsn  48903  resinsnALT  48904  opndisj  48934  istermc  49506  lanrcl  49653  ranrcl  49654