Theorem eqeq1i 2741

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 2740	. 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 2708

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

This theorem is referenced by:  eqeq12i  2754  eqabb  2875  neeq1i  2996  dfss2  3907  ssequn2  4129  ineqcom  4150  dfss7  4191  dfss4  4209  rabeq0w  4327  rabeq0  4328  disj  4390  undisj1  4402  undisj2  4403  undif  4422  undifr  4423  rabeqsn  4611  reusn  4671  rabsneu  4673  eusn  4674  tppreqb  4750  elpreqpr  4810  uniintsn  4927  iin0  5304  dfepfr  5615  epfrc  5616  dmopab3  5874  dm0rn0  5879  dm0rn0OLD  5880  rnopab3  5911  ssdmres  5978  iresn0n0  6019  imadisj  6045  args  6057  dffr3  6064  intirr  6081  dminxp  6144  dfrel3  6162  coeq0  6220  snres0  6262  sspred  6274  dffr4  6284  frpomin2  6305  frpoind  6306  cbviotavw  6462  fntpg  6558  fncnv  6571  mptfnf  6633  sbcfng  6665  f0rn0  6725  dff1o4  6788  dffv4  6837  tz6.12c  6862  fvun2  6932  fnreseql  7000  funopdmsn  7104  riota1  7345  riota2df  7347  riotaeqimp  7350  fnbrovb  7418  ovid  7508  ov  7511  ovg  7532  ovima0  7546  opiota  8012  frrlem13  8248  tz7.49c  8385  sucprcreg  9520  sucprcregOLD  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  11455  addeq0  11573  elznn0  12539  xrsupss  13261  xrinfmss  13262  prinfzo0  13653  seqf1olem1  14003  seqf1olem2  14004  sqeqori  14176  hashrabsn1  14336  hashprb  14359  hashprdifel  14360  hashbclem  14414  hash2pwpr  14438  f1oun2prg  14879  modfsummods  15756  cshwrepswhash1  17073  ismgmid  18633  smndex2dnrinv  18886  oppgid  19331  lsmdisjr  19659  gexex  19828  gsumxp2  19955  dprd0  20008  oppr1  20330  opprunit  20357  zringndrg  21448  gsummoncoe1  22273  mat0dimcrng  22435  iinopn  22867  elcls  23038  ordthaus  23349  hauscmplem  23371  regr1lem2  23705  metdseq0  24820  minveclem1  25391  minveclem3b  25395  volun  25512  dyaddisj  25563  vieta1  26278  logeftb  26547  birthdaylem1  26915  dmgmaddn0  26986  gausslemma2d  27337  lgseisenlem1  27338  2lgslem4  27369  rpvmasum  27489  ltssolem1  27639  noinfbnd2lem1  27694  madeval2  27825  made0  27855  axsegconlem6  28991  edg0iedg0  29124  numedglnl  29213  ushgredgedg  29298  ushgredgedgloop  29300  uhgr0v0e  29307  usgr1v0edg  29326  usgrexmpllem  29329  usgr1v0e  29395  nbuhgr2vtx1edgblem  29420  uvtx01vtx  29466  prcliscplgr  29483  cusgr0v  29497  vtxdg0e  29543  1loopgrvd2  29572  finsumvtxdg2ssteplem4  29617  finsumvtxdg2size  29619  isrgr  29628  fusgrregdegfi  29638  wspn0  29992  2wlkdlem8  30001  3wlkdlem8  30237  uhgr3cyclexlem  30251  1to2vfriswmgr  30349  1to3vfriswmgr  30350  frgrregorufr0  30394  frgrreg  30464  frgrregord013  30465  ex-ceil  30518  nmlno0lem  30864  minvecolem1  30945  hvsubeq0i  31134  hvsubaddi  31137  pjoc2i  31509  pjoml3i  31657  cmbr3i  31671  pjss2i  31751  hosubeq0i  31897  dmadjrnb  31977  nmlnop0iALT  32066  nmopcoadj0i  32174  stm1ri  32315  jplem2  32340  atoml2i  32454  chirredlem1  32461  cdj3lem3  32509  difininv  32587  disjnf  32640  disjpreima  32654  disjunsn  32664  f1od2  32792  wrdt2ind  33013  isunit2  33301  isdrng4  33356  lsmsnorb2  33452  ssdifidlprm  33518  fldext2chn  33872  zrhchr  34118  ddemeas  34380  braew  34386  aean  34388  eulerpartlemgh  34522  ballotlemfp1  34636  repr0  34755  hgt750lem2  34796  bnj1143  34932  nummin  35236  acycgr0v  35330  prclisacycgr  35333  cvmsss2  35456  cvmlift2lem13  35497  elrn3  35944  rankeq1o  36353  hfun  36360  bj-disj2r  37335  bj-sscon  37336  bj-0int  37413  bj-imdirco  37504  bj-pinftynminfty  37541  finxpreclem4  37710  nlpineqsn  37724  curunc  37923  tan2h  37933  poimirlem13  37954  poimirlem14  37955  poimirlem21  37962  poimirlem22  37963  asindmre  38024  totbndbnd  38110  rngosn3  38245  scott0f  38490  n0el2  38656  dfrel5  38667  dfrel6  38668  redundeq1  39034  dmqscoelseq  39067  dfeldisj5  39134  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  lhpbase  40444  cdlemg31b0N  41140  cdlemg31b0a  41141  cdlemh  41263  sticksstones16  42601  sticksstones21  42606  unitscyglem3  42636  onsupmaxb  43667  iunrelexp0  44129  frege120  44410  clsk1indlem4  44471  gneispace  44561  scotteld  44673  undisjrab  44733  zfregs2VD  45267  dvnprod  46377  fnresfnco  47489  aiotavb  47538  afvpcfv0  47594  aovpcov0  47638  aov0ov0  47641  aovov0bi  47644  fnotaovb  47646  funressndmafv2rn  47671  fmtnoprmfac1lem  48027  lighneallem2  48069  stgrvtx0  48438  isubgr3stgrlem6  48447  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  snlindsntor  48947  rrx2pnedifcoorneorr  49193  itschlc0xyqsol1  49242  2itscp  49257  resinsn  49347  resinsnALT  49348  opndisj  49378  istermc  49949  lanrcl  50096  ranrcl  50097