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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  eqeq12i  2755  eqabb  2876  neeq1i  2997  dfss2  3921  ssequn2  4143  ineqcom  4164  sseqin2  4177  dfss7  4205  dfss4  4223  rabeq0w  4341  rabeq0  4342  disj  4404  disjr  4405  undisj1  4416  undisj2  4417  undif  4436  undifr  4437  undifrOLD  4438  uneqdifeq  4447  rabeqsn  4626  reusn  4686  rabsneu  4688  eusn  4689  tppreqb  4763  elpreqpr  4825  uniintsn  4942  iin0  5309  dfepfr  5616  epfrc  5617  dmopab3  5876  dm0rn0  5881  dm0rn0OLD  5882  rnopab3  5913  ssdmres  5980  iresn0n0  6021  imadisj  6047  args  6059  dffr3  6066  intirr  6083  dminxp  6146  dfrel3  6164  coeq0  6222  snres0  6264  sspred  6276  dffr4  6286  frpomin2  6307  frpoind  6308  cbviotavw  6464  fntpg  6560  fncnv  6573  mptfnf  6635  sbcfng  6667  f0rn0  6727  dff1o4  6790  dffv4  6839  tz6.12c  6864  fvun2  6934  fnreseql  7002  funopdmsn  7105  riota1  7346  riota2df  7348  riotaeqimp  7351  fnbrovb  7419  ovid  7509  ov  7512  ovg  7533  ovima0  7547  opiota  8013  frrlem13  8250  tz7.49c  8387  sucprcreg  9521  zfregfr  9525  inf3lem2  9550  zfregs2  9654  frind  9674  rankxpsuc  9806  scott0s  9812  cplem1  9813  cfslb2n  10190  fin23lem26  10247  dfacfin7  10321  axdc3lem4  10375  zorn2lem7  10424  alephom  10508  fpwwe2  10566  recmulnq  10887  recexsr  11030  map2psrpr  11033  renegcli  11454  addeq0  11572  elznn0  12515  xrsupss  13236  xrinfmss  13237  prinfzo0  13626  seqf1olem1  13976  seqf1olem2  13977  sqeqori  14149  hashrabsn1  14309  hashprb  14332  hashprdifel  14333  hashbclem  14387  hash2pwpr  14411  f1oun2prg  14852  modfsummods  15728  cshwrepswhash1  17042  ismgmid  18602  smndex2dnrinv  18852  oppgid  19297  lsmdisjr  19625  gexex  19794  gsumxp2  19921  dprd0  19974  oppr1  20298  opprunit  20325  zringndrg  21435  gsummoncoe1  22264  mat0dimcrng  22426  iinopn  22858  elcls  23029  ordthaus  23340  hauscmplem  23362  regr1lem2  23696  metdseq0  24811  minveclem1  25392  minveclem3b  25396  volun  25514  dyaddisj  25565  vieta1  26288  logeftb  26560  birthdaylem1  26929  dmgmaddn0  27001  gausslemma2d  27353  lgseisenlem1  27354  2lgslem4  27385  rpvmasum  27505  ltssolem1  27655  noinfbnd2lem1  27710  madeval2  27841  made0  27871  axsegconlem6  29007  edg0iedg0  29140  numedglnl  29229  ushgredgedg  29314  ushgredgedgloop  29316  uhgr0v0e  29323  usgr1v0edg  29342  usgrexmpllem  29345  usgr1v0e  29411  nbuhgr2vtx1edgblem  29436  uvtx01vtx  29482  prcliscplgr  29499  cusgr0v  29513  vtxdg0e  29560  1loopgrvd2  29589  finsumvtxdg2ssteplem4  29634  finsumvtxdg2size  29636  isrgr  29645  fusgrregdegfi  29655  wspn0  30009  2wlkdlem8  30018  3wlkdlem8  30254  uhgr3cyclexlem  30268  1to2vfriswmgr  30366  1to3vfriswmgr  30367  frgrregorufr0  30411  frgrreg  30481  frgrregord013  30482  ex-ceil  30535  nmlno0lem  30881  minvecolem1  30962  hvsubeq0i  31151  hvsubaddi  31154  pjoc2i  31526  pjoml3i  31674  cmbr3i  31688  pjss2i  31768  hosubeq0i  31914  dmadjrnb  31994  nmlnop0iALT  32083  nmopcoadj0i  32191  stm1ri  32332  jplem2  32357  atoml2i  32471  chirredlem1  32478  cdj3lem3  32526  difininv  32604  disjnf  32657  disjpreima  32671  disjunsn  32681  f1od2  32809  wrdt2ind  33046  isunit2  33334  isdrng4  33389  lsmsnorb2  33485  ssdifidlprm  33551  fldext2chn  33906  zrhchr  34152  ddemeas  34414  braew  34420  aean  34422  eulerpartlemgh  34556  ballotlemfp1  34670  repr0  34789  hgt750lem2  34830  bnj1143  34966  nummin  35270  acycgr0v  35364  prclisacycgr  35367  cvmsss2  35490  cvmlift2lem13  35531  elrn3  35978  rankeq1o  36387  hfun  36394  bj-disj2r  37276  bj-sscon  37277  bj-0int  37354  bj-imdirco  37445  bj-pinftynminfty  37482  finxpreclem4  37649  nlpineqsn  37663  curunc  37853  tan2h  37863  poimirlem13  37884  poimirlem14  37885  poimirlem21  37892  poimirlem22  37893  asindmre  37954  totbndbnd  38040  rngosn3  38175  scott0f  38420  n0el2  38586  dfrel5  38597  dfrel6  38598  redundeq1  38964  dmqscoelseq  38997  dfeldisj5  39064  atbase  39665  llnbase  39885  lplnbase  39910  lvolbase  39954  lhpbase  40374  cdlemg31b0N  41070  cdlemg31b0a  41071  cdlemh  41193  sticksstones16  42532  sticksstones21  42537  unitscyglem3  42567  onsupmaxb  43596  iunrelexp0  44058  frege120  44339  clsk1indlem4  44400  gneispace  44490  scotteld  44602  undisjrab  44662  zfregs2VD  45196  dvnprod  46307  fnresfnco  47401  aiotavb  47450  afvpcfv0  47506  aovpcov0  47550  aov0ov0  47553  aovov0bi  47556  fnotaovb  47558  funressndmafv2rn  47583  fmtnoprmfac1lem  47924  lighneallem2  47966  stgrvtx0  48322  isubgr3stgrlem6  48331  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  snlindsntor  48831  rrx2pnedifcoorneorr  49077  itschlc0xyqsol1  49126  2itscp  49141  resinsn  49231  resinsnALT  49232  opndisj  49262  istermc  49833  lanrcl  49980  ranrcl  49981