Theorem eqeq1i 2734

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq12i  2747  eqabb  2867  neeq1i  2989  dfss2  3929  ssequn2  4148  ineqcom  4169  sseqin2  4182  dfss7  4210  dfss4  4228  rabeq0w  4346  rabeq0  4347  disj  4409  disjr  4410  undisj1  4421  undisj2  4422  undif  4441  undifr  4442  undifrOLD  4443  uneqdifeq  4452  rabeqsn  4627  reusn  4687  rabsneu  4689  eusn  4690  tppreqb  4765  elpreqpr  4827  uniintsn  4945  iin0  5312  dfepfr  5615  epfrc  5616  dmopab3  5873  dm0rn0  5878  rnopab3  5909  ssdmres  5973  iresn0n0  6014  imadisj  6040  args  6052  dffr3  6059  intirr  6079  dminxp  6141  dfrel3  6159  coeq0  6216  snres0  6259  sspred  6271  dffr4  6281  frpomin2  6302  frpoind  6303  cbviotavw  6460  fntpg  6560  fncnv  6573  mptfnf  6635  sbcfng  6667  f0rn0  6727  dff1o4  6790  dffv4  6837  tz6.12c  6862  fvun2  6935  fnreseql  7002  funopdmsn  7104  riota1  7347  riota2df  7349  riotaeqimp  7352  fnbrovb  7420  ovid  7510  ov  7513  ovg  7534  ovima0  7548  opiota  8017  frrlem13  8254  tz7.49c  8391  sucprcreg  9530  zfregfr  9534  inf3lem2  9558  zfregs2  9662  frind  9679  rankxpsuc  9811  scott0s  9817  cplem1  9818  cfslb2n  10197  fin23lem26  10254  dfacfin7  10328  axdc3lem4  10382  zorn2lem7  10431  alephom  10514  fpwwe2  10572  recmulnq  10893  recexsr  11036  map2psrpr  11039  renegcli  11459  addeq0  11577  elznn0  12520  xrsupss  13245  xrinfmss  13246  prinfzo0  13635  seqf1olem1  13982  seqf1olem2  13983  sqeqori  14155  hashrabsn1  14315  hashprb  14338  hashprdifel  14339  hashbclem  14393  hash2pwpr  14417  f1oun2prg  14859  modfsummods  15735  cshwrepswhash1  17049  ismgmid  18568  smndex2dnrinv  18818  oppgid  19264  lsmdisjr  19590  gexex  19759  gsumxp2  19886  dprd0  19939  oppr1  20235  opprunit  20262  zringndrg  21354  gsummoncoe1  22171  mat0dimcrng  22333  iinopn  22765  elcls  22936  ordthaus  23247  hauscmplem  23269  regr1lem2  23603  metdseq0  24719  minveclem1  25300  minveclem3b  25304  volun  25422  dyaddisj  25473  vieta1  26196  logeftb  26468  birthdaylem1  26837  dmgmaddn0  26909  gausslemma2d  27261  lgseisenlem1  27262  2lgslem4  27293  rpvmasum  27413  sltsolem1  27563  noinfbnd2lem1  27618  madeval2  27737  made0  27761  axsegconlem6  28825  edg0iedg0  28958  numedglnl  29047  ushgredgedg  29132  ushgredgedgloop  29134  uhgr0v0e  29141  usgr1v0edg  29160  usgrexmpllem  29163  usgr1v0e  29229  nbuhgr2vtx1edgblem  29254  uvtx01vtx  29300  prcliscplgr  29317  cusgr0v  29331  vtxdg0e  29378  1loopgrvd2  29407  finsumvtxdg2ssteplem4  29452  finsumvtxdg2size  29454  isrgr  29463  fusgrregdegfi  29473  wspn0  29827  2wlkdlem8  29836  3wlkdlem8  30069  uhgr3cyclexlem  30083  1to2vfriswmgr  30181  1to3vfriswmgr  30182  frgrregorufr0  30226  frgrreg  30296  frgrregord013  30297  ex-ceil  30350  nmlno0lem  30695  minvecolem1  30776  hvsubeq0i  30965  hvsubaddi  30968  pjoc2i  31340  pjoml3i  31488  cmbr3i  31502  pjss2i  31582  hosubeq0i  31728  dmadjrnb  31808  nmlnop0iALT  31897  nmopcoadj0i  32005  stm1ri  32146  jplem2  32171  atoml2i  32285  chirredlem1  32292  cdj3lem3  32340  difininv  32419  disjnf  32472  disjpreima  32486  disjunsn  32496  f1od2  32617  wrdt2ind  32848  isunit2  33164  isdrng4  33218  lsmsnorb2  33336  ssdifidlprm  33402  fldext2chn  33691  zrhchr  33937  ddemeas  34199  braew  34205  aean  34207  eulerpartlemgh  34342  ballotlemfp1  34456  repr0  34575  hgt750lem2  34616  bnj1143  34753  nummin  35054  acycgr0v  35108  prclisacycgr  35111  cvmsss2  35234  cvmlift2lem13  35275  elrn3  35722  rankeq1o  36132  hfun  36139  bj-disj2r  36989  bj-sscon  36990  bj-0int  37062  bj-imdirco  37151  bj-pinftynminfty  37188  finxpreclem4  37355  nlpineqsn  37369  curunc  37569  tan2h  37579  poimirlem13  37600  poimirlem14  37601  poimirlem21  37608  poimirlem22  37609  asindmre  37670  totbndbnd  37756  rngosn3  37891  scott0f  38136  n0el2  38290  dfrel5  38301  dfrel6  38302  redundeq1  38593  dmqscoelseq  38626  dfeldisj5  38686  atbase  39255  llnbase  39476  lplnbase  39501  lvolbase  39545  lhpbase  39965  cdlemg31b0N  40661  cdlemg31b0a  40662  cdlemh  40784  sticksstones16  42123  sticksstones21  42128  unitscyglem3  42158  onsupmaxb  43201  iunrelexp0  43664  frege120  43945  clsk1indlem4  44006  gneispace  44096  scotteld  44208  undisjrab  44268  zfregs2VD  44803  dvnprod  45920  fnresfnco  47015  aiotavb  47064  afvpcfv0  47120  aovpcov0  47164  aov0ov0  47167  aovov0bi  47170  fnotaovb  47172  funressndmafv2rn  47197  fmtnoprmfac1lem  47538  lighneallem2  47580  stgrvtx0  47934  isubgr3stgrlem6  47943  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  snlindsntor  48433  rrx2pnedifcoorneorr  48679  itschlc0xyqsol1  48728  2itscp  48743  resinsn  48833  resinsnALT  48834  opndisj  48864  istermc  49436  lanrcl  49583  ranrcl  49584