Theorem eqeq1i 2744

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

Syntax hints:   ↔ wb 205   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  eqeq12i  2757  neeq1i  3009  ssequn2  4121  ineqcom  4141  sseqin2  4154  dfss7  4179  dfss4  4197  rabeq0w  4322  rabeq0  4323  disj  4386  disjOLD  4387  disjr  4388  undisj1  4400  undisj2  4401  undif  4420  uneqdifeq  4428  rabeqsn  4607  reusn  4668  rabsneu  4670  eusn  4671  tppreqb  4743  elpreqpr  4802  uniintsn  4923  iin0  5287  dfepfr  5573  epfrc  5574  dmopab3  5825  dm0rn0  5831  ssdmres  5911  iresn0n0  5960  imadisj  5985  args  5997  dffr3  6004  intirr  6020  dminxp  6080  dfrel3  6098  coeq0  6156  sspred  6208  dffr4  6219  frpomin2  6241  frpoind  6242  tz6.26OLD  6248  wfiOLD  6251  unisuc  6339  cbviotavw  6396  fntpg  6490  fncnv  6503  mptfnf  6564  sbcfng  6593  f0rn0  6655  dff1o4  6720  dffv4  6765  fvun2  6854  fnreseql  6919  funopdmsn  7016  f1ofvswap  7171  riota1  7247  riota2df  7249  riotaeqimp  7252  fnbrovb  7317  ovid  7405  ov  7408  ovg  7428  ovima0  7442  opiota  7885  frrlem13  8098  wfrlem8OLD  8131  tz7.49c  8261  sucprcreg  9321  zfregfr  9324  inf3lem2  9348  zfregs2  9474  frind  9492  rankxpsuc  9624  scott0s  9630  cplem1  9631  cfslb2n  10008  fin23lem26  10065  dfacfin7  10139  axdc3lem4  10193  zorn2lem7  10242  alephom  10325  fpwwe2  10383  recmulnq  10704  recexsr  10847  map2psrpr  10850  renegcli  11265  addeq0  11381  elznn0  12317  xrsupss  13025  xrinfmss  13026  prinfzo0  13407  seqf1olem1  13743  seqf1olem2  13744  sqeqori  13911  hashrabsn1  14070  hashprb  14093  hashprdifel  14094  hashbclem  14145  hash2pwpr  14171  f1oun2prg  14611  modfsummods  15486  cshwrepswhash1  16785  ismgmid  18330  smndex2dnrinv  18535  oppgid  18944  lsmdisjr  19271  gexex  19435  gsumxp2  19562  dprd0  19615  oppr1  19857  opprunit  19884  opprdomn  20553  zringndrg  20671  gsummoncoe1  21456  mat0dimcrng  21600  iinopn  22032  elcls  22205  ordthaus  22516  hauscmplem  22538  regr1lem2  22872  metdseq0  23998  minveclem1  24569  minveclem3b  24573  volun  24690  dyaddisj  24741  vieta1  25453  logeftb  25720  birthdaylem1  26082  dmgmaddn0  26153  gausslemma2d  26503  lgseisenlem1  26504  2lgslem4  26535  rpvmasum  26655  axsegconlem6  27271  edg0iedg0  27406  numedglnl  27495  ushgredgedg  27577  ushgredgedgloop  27579  uhgr0v0e  27586  usgr1v0edg  27605  usgrexmpllem  27608  usgr1v0e  27674  nbuhgr2vtx1edgblem  27699  uvtx01vtx  27745  prcliscplgr  27762  cusgr0v  27776  vtxdg0e  27822  1loopgrvd2  27851  finsumvtxdg2ssteplem4  27896  finsumvtxdg2size  27898  isrgr  27907  fusgrregdegfi  27917  wspn0  28268  2wlkdlem8  28277  3wlkdlem8  28510  uhgr3cyclexlem  28524  1to2vfriswmgr  28622  1to3vfriswmgr  28623  frgrregorufr0  28667  frgrreg  28737  frgrregord013  28738  ex-ceil  28791  nmlno0lem  29134  minvecolem1  29215  hvsubeq0i  29404  hvsubaddi  29407  pjoc2i  29779  pjoml3i  29927  cmbr3i  29941  pjss2i  30021  hosubeq0i  30167  dmadjrnb  30247  nmlnop0iALT  30336  nmopcoadj0i  30444  stm1ri  30585  jplem2  30610  atoml2i  30724  chirredlem1  30731  cdj3lem3  30779  difininv  30843  undifr  30851  disjnf  30888  disjpreima  30902  disjunsn  30912  f1od2  31035  wrdt2ind  31204  lsmsnorb2  31559  zrhchr  31905  ddemeas  32183  braew  32189  aean  32191  eulerpartlemgh  32324  ballotlemfp1  32437  repr0  32570  hgt750lem2  32611  bnj1143  32749  nummin  33042  acycgr0v  33089  prclisacycgr  33092  cvmsss2  33215  cvmlift2lem13  33256  snres0  33654  elrn3  33708  sltsolem1  33857  noinfbnd2lem1  33912  madeval2  34016  made0  34036  rankeq1o  34452  hfun  34459  bj-disj2r  35197  bj-sscon  35198  bj-0int  35251  bj-imdirco  35340  bj-pinftynminfty  35377  finxpreclem4  35544  nlpineqsn  35558  curunc  35738  tan2h  35748  poimirlem13  35769  poimirlem14  35770  poimirlem21  35777  poimirlem22  35778  asindmre  35839  totbndbnd  35926  rngosn3  36061  scott0f  36306  n0el2  36447  dfrel5  36460  dfrel6  36461  redundeq1  36721  dmqscoelseq  36752  dfeldisj5  36811  atbase  37282  llnbase  37502  lplnbase  37527  lvolbase  37571  lhpbase  37991  cdlemg31b0N  38687  cdlemg31b0a  38688  cdlemh  38810  sticksstones16  40098  sticksstones21  40103  metakunt24  40128  iunrelexp0  41263  frege120  41544  clsk1indlem4  41607  gneispace  41697  scotteld  41817  undisjrab  41877  zfregs2VD  42414  dvnprod  43444  fnresfnco  44486  aiotavb  44533  afvpcfv0  44589  aovpcov0  44633  aov0ov0  44636  aovov0bi  44639  fnotaovb  44641  funressndmafv2rn  44666  fmtnoprmfac1lem  44968  lighneallem2  45010  snlindsntor  45764  rrx2pnedifcoorneorr  46015  itschlc0xyqsol1  46064  2itscp  46079  opndisj  46148