Theorem eqeq1i 2778

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

Syntax hints:   ↔ wb 198   = wceq 1508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2766

This theorem is referenced by:  eqeq12i  2787  neeq1i  3026  ssequn2  4042  sseqin2  4074  dfss7  4099  dfss4  4117  rabeq0  4219  disj  4277  disjr  4278  undisj1  4289  undisj2  4290  undif  4308  uneqdifeq  4316  rabeqsn  4475  reusn  4534  rabsneu  4536  eusn  4537  tppreqb  4609  elpreqpr  4668  uniintsn  4783  iin0  5112  dfepfr  5389  epfrc  5390  dmopab3  5633  dm0rn0  5638  ssdmres  5719  imadisj  5786  args  5795  dffr3  5800  intirr  5816  dminxp  5875  dfrel3  5892  coeq0  5945  sspred  5992  dffr4  6000  tz6.26  6015  wfi  6017  unisuc  6103  fntpg  6245  fncnv  6258  mptfnf  6311  sbcfng  6339  f0rn0  6391  dff1o4  6450  dffv4  6494  fvun2  6582  fnreseql  6642  funopdmsn  6734  riota1  6954  riota2df  6956  riotaeqimp  6959  fnbrovb  7023  ovid  7106  ov  7109  ovg  7128  ovima0  7142  opiota  7564  wfrlem8  7765  tz7.49c  7884  sucprcreg  8859  zfregfr  8862  inf3lem2  8885  zfregs2  8968  rankxpsuc  9104  scott0s  9110  cplem1  9111  cfslb2n  9487  fin23lem26  9544  dfacfin7  9618  axdc3lem4  9672  zorn2lem7  9721  alephom  9804  fpwwe2  9862  recmulnq  10183  recexsr  10326  map2psrpr  10329  renegcli  10747  addeq0  10863  elznn0  11807  xrsupss  12517  xrinfmss  12518  prinfzo0  12890  seqf1olem1  13223  seqf1olem2  13224  sqeqori  13390  hashrabsn1  13547  hashprb  13570  hashprdifel  13571  hashbclem  13622  hash2pwpr  13644  swrdccat3aOLD  13942  f1oun2prg  14140  modfsummods  15007  cshwrepswhash1  16291  ismgmid  17745  oppgid  18268  lsmdisjr  18581  gexex  18742  dprd0  18916  oppr1  19120  opprunit  19147  opprdomn  19808  gsummoncoe1  20191  zringndrg  20355  mat0dimcrng  20799  iinopn  21230  elcls  21401  ordthaus  21712  hauscmplem  21734  regr1lem2  22068  metdseq0  23181  minveclem1  23746  minveclem3b  23750  volun  23865  dyaddisj  23916  vieta1  24620  logeftb  24884  birthdaylem1  25247  dmgmaddn0  25318  gausslemma2d  25668  lgseisenlem1  25669  2lgslem4  25700  rpvmasum  25820  axsegconlem6  26427  edg0iedg0  26559  numedglnl  26648  ushgredgedg  26730  ushgredgedgloop  26732  uhgr0v0e  26739  usgr1v0edg  26758  usgrexmpllem  26761  usgr1v0e  26827  nbuhgr2vtx1edgblem  26852  uvtx01vtx  26898  prcliscplgr  26915  cusgr0v  26929  vtxdg0e  26975  1loopgrvd2  27004  finsumvtxdg2ssteplem4  27049  finsumvtxdg2size  27051  isrgr  27060  fusgrregdegfi  27070  wspn0  27446  2wlkdlem8  27455  3wlkdlem8  27712  uhgr3cyclexlem  27726  1to2vfriswmgr  27829  1to3vfriswmgr  27830  frgrregorufr0  27874  frgrreg  27967  frgrregord013  27968  ex-ceil  28021  nmlno0lem  28363  minvecolem1  28445  hvsubeq0i  28635  hvsubaddi  28638  pjoc2i  29012  pjoml3i  29160  cmbr3i  29174  pjss2i  29254  hosubeq0i  29400  dmadjrnb  29480  nmlnop0iALT  29569  nmopcoadj0i  29677  stm1ri  29818  jplem2  29843  atoml2i  29957  chirredlem1  29964  cdj3lem3  30012  difininv  30071  disjnf  30105  disjpreima  30118  disjunsn  30128  f1od2  30234  wrdt2ind  30393  zrhchr  30894  ddemeas  31173  braew  31179  aean  31181  eulerpartlemgh  31314  ballotlemfp1  31428  repr0  31563  hgt750lem2  31604  bnj1143  31743  cvmsss2  32139  cvmlift2lem13  32180  elrn3  32551  frpomin2  32633  frpoind  32634  frind  32639  frrlem13  32689  sltsolem1  32734  madeval2  32844  rankeq1o  33186  hfun  33193  bj-disj2r  33888  bj-sscon  33889  bj-0int  33936  bj-pinftynminfty  34011  finxpreclem4  34149  nlpineqsn  34163  curunc  34348  tan2h  34358  poimirlem13  34379  poimirlem14  34380  poimirlem21  34387  poimirlem22  34388  asindmre  34451  totbndbnd  34542  rngosn3  34677  scott0f  34924  ineqcom  34981  n0el2  35068  dfrel5  35082  dfrel6  35083  redundeq1  35342  dmqscoelseq  35373  dfeldisj5  35432  atbase  35903  llnbase  36123  lplnbase  36148  lvolbase  36192  lhpbase  36612  cdlemg31b0N  37308  cdlemg31b0a  37309  cdlemh  37431  iunrelexp0  39444  frege120  39726  clsk1indlem4  39791  gneispace  39881  scotteld  39991  undisjrab  40088  zfregs2VD  40628  dvnprod  41694  fnresfnco  42711  aiotavb  42726  afvpcfv0  42781  aovpcov0  42825  aov0ov0  42828  aovov0bi  42831  fnotaovb  42833  funressndmafv2rn  42858  fmtnoprmfac1lem  43124  lighneallem2  43169  snlindsntor  43923  rrx2pnedifcoorneorr  44102  itschlc0xyqsol1  44151  2itscp  44166