Theorem eqeq2i 2834

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq2i	⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq2 2833	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  eqeq12i  2836  eqtri  2844  neeq2i  3081  rabid2  3381  rabid2f  3382  dfss2  3954  equncom  4129  absn  4578  rabrsn  4653  ssunpr  4758  sspr  4759  sstp  4760  preq12b  4774  preqsnd  4782  preq12nebg  4786  opthprneg  4788  opeqpr  5387  propssopi  5390  wefrc  5543  dfrel4v  6041  dfrel4  6042  orddif  6278  funopg  6383  funimaexg  6434  funcocnv2  6633  dffn5f  6730  fnressn  6914  fressnfv  6916  fnprb  6965  fntpb  6966  riotaeqimp  7134  fnov  7276  ovmpos  7292  onuninsuci  7549  fvresex  7655  elxp6  7717  el2xptp  7729  el2xptp0  7730  opiota  7751  tpossym  7918  qsid  8357  mapsncnv  8451  ixpsnf1o  8496  card1  9391  pm54.43lem  9422  cf0  9667  sdom2en01  9718  cardeq0  9968  enqbreq2  10336  addcompr  10437  mulcompr  10439  axrrecex  10579  negeq0  10934  muleqadd  11278  crne0  11625  dfnn3  11646  xmulneg1  12656  hasheq0  13718  hashbc  13805  hashf1lem2  13808  hash2pwpr  13828  eqwrds3  14319  cjne0  14516  sqrt00  14617  sqrtmsq2i  14741  cbvsum  15046  fsump1i  15118  cbvprod  15263  bpoly2  15405  bpoly3  15406  bpoly4  15407  absefib  15545  efieq1re  15546  xpccatid  17432  sgrpidmnd  17910  smndex2dnrinv  18074  isnsg4  18313  selvval  20325  mat1dimelbas  21074  pmatcollpw3fi1lem1  21388  2ndcctbss  22057  ptcnp  22224  ovolgelb  24075  ioorinv  24171  rolle  24581  plymul0or  24864  reeff1o  25029  sineq0  25103  coseq1  25104  1cubr  25414  atandm2  25449  atandm3  25450  efrlim  25541  isppw  25685  ppiub  25774  lgsdinn0  25915  m1lgs  25958  uhgr2edg  26984  usgredg2vlem1  27001  usgredg2vlem2  27002  ushgredgedg  27005  ushgredgedgloop  27007  edgnbusgreu  27143  nb3grprlem2  27157  nb3gr2nb  27160  usgredgsscusgredg  27235  usgr2wlkneq  27531  usgr2pthlem  27538  crctcshwlkn0  27593  wwlksn0s  27633  umgr2adedgwlk  27718  umgr2adedgspth  27721  elwwlks2s3  27724  elwwlks2ons3im  27727  rusgrnumwwlkl1  27741  clwlkclwwlkflem  27776  isfrgr  28033  frgr3v  28048  frgrregorufr0  28097  isgrpo  28268  vciOLD  28332  chnlei  29256  h1de2ctlem  29326  cmcmlem  29362  cmcm2i  29364  cmbr2i  29367  osumcor2i  29415  pjss2i  29451  ho01i  29599  nmop0h  29762  pjclem1  29966  jplem1  30039  atabs2i  30173  fedgmullem2  31021  ccfldextdgrr  31052  breprexp  31899  bnj168  31995  bnj927  32035  bnj543  32160  bnj970  32214  subfacp1lem6  32427  satfv1  32605  satfvsucsuc  32607  satf0  32614  fmlaomn0  32632  fmla0disjsuc  32640  satffunlem2lem1  32646  mppspstlem  32813  quad3  32908  trpredmintr  33065  brdomain  33389  brrange  33390  brimg  33393  brapply  33394  brsuccf  33397  brfullfun  33404  brrestrict  33405  rankeq1o  33627  bj-snsetex  34270  bj-reabeq  34334  bj-rest10  34373  bj-ismooredr2  34396  bj-pinftynminfty  34503  dffinxpf  34660  finxp0  34666  matunitlindflem1  34882  ismblfin  34927  opropabco  34993  fdc  35014  isdrngo1  35228  smprngopr  35324  cdleme25cv  37488  cdlemk35  38042  dicval2  38309  dicopelval2  38311  dicelval2N  38312  hdmap1fval  38926  mzpcompact2lem  39341  eldioph4b  39401  2nn0ind  39535  islmodfg  39662  relintab  39936  brtrclfv2  40065  frege116  40318  elnev  40763  dvnprodlem1  42224  fourierdlem103  42488  fourierdlem104  42489  ovnovollem3  42934  fmtno4prmfac  43728  lindsrng01  44517  ldepspr  44522  nn0sumshdiglemB  44674