Theorem eqeq2i 2775

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

Syntax hints:   ↔ wb 208   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  eqeq12i  2780  eqtri  2785  neeq2i  3022  rabid2f  3445  rabid2im  3446  abv  3466  equncom  4112  eq0  4302  ab0w  4332  ab0  4333  ab0orv  4336  absn  4602  rabrsn  4683  ssunpr  4792  sspr  4793  sstp  4794  preq12b  4808  preqsnd  4817  preq12nebg  4821  opthprneg  4823  opeqpr  5474  propssopi  5477  wefrc  5641  dfrel4v  6176  dfrel4  6177  orddif  6444  funopg  6555  f1imadifssran  6607  funcocnv2  6832  dffn5f  6938  fnressn  7141  fressnfv  7143  fnprb  7192  fntpb  7193  riotaeqimp  7379  fnov  7527  ovmpos  7544  onuninsuci  7820  fvresex  7941  elxp6  8004  el2xptp  8016  el2xptp0  8017  opiota  8040  tpossym  8238  qsid  8763  mapsncnv  8875  ixpsnf1o  8920  card1  9926  pm54.43lem  9958  cf0  10207  sdom2en01  10259  cardeq0  10509  enqbreq2  10878  addcompr  10979  mulcompr  10981  axrrecex  11121  negeq0  11485  muleqadd  11831  crne0  12188  dfnn3  12224  xmulneg1  13272  hasheq0  14376  hashbc  14466  hashf1lem2  14469  hash2pwpr  14489  eqwrds3  14974  cjne0  15190  sqrt00  15290  sqrtmsq2i  15415  cbvsum  15722  cbvsumv  15723  fsump1i  15796  cbvprod  15943  cbvprodv  15944  bpoly2  16087  bpoly3  16088  bpoly4  16089  absefib  16230  efieq1re  16231  xpccatid  18220  sgrpidmnd  18773  smndex2dnrinv  18952  isnsg4  19208  opprdomnb  20767  selvval  22173  mat1dimelbas  22531  pmatcollpw3fi1lem1  22846  2ndcctbss  23515  ptcnp  23682  ovolgelb  25542  ioorinv  25638  dvcobr  26008  rolle  26052  dvfsumlem2  26089  plymul0or  26342  reeff1o  26510  sineq0  26589  coseq1  26590  1cubr  26907  atandm2  26942  atandm3  26943  efrlim  27034  isppw  27178  ppiub  27268  lgsdinn0  27409  m1lgs  27452  elzs2  28492  elznns  28495  twocut  28516  uhgr2edg  29409  usgredg2vlem1  29426  usgredg2vlem2  29427  ushgredgedg  29430  ushgredgedgloop  29432  edgnbusgreu  29568  nb3grprlem2  29582  nb3gr2nb  29585  usgredgsscusgredg  29660  usgr2wlkneq  29956  usgr2pthlem  29963  crctcshwlkn0  30021  wwlksn0s  30061  umgr2adedgwlk  30145  umgr2adedgspth  30148  elwwlks2s3  30151  elwwlks2ons3im  30154  rusgrnumwwlkl1  30171  clwlkclwwlkflem  30206  isfrgr  30462  frgr3v  30477  frgrregorufr0  30526  isgrpo  30700  vciOLD  30764  chnlei  31688  h1de2ctlem  31758  cmcmlem  31794  cmcm2i  31796  cmbr2i  31799  osumcor2i  31847  pjss2i  31883  ho01i  32031  nmop0h  32194  pjclem1  32398  jplem1  32471  atabs2i  32605  1arithidom  33733  ply1dg1rt  33776  selvply1rhmlem2  33818  esplyfval1  33870  vieta  33877  fedgmullem2  33927  ccfldextdgrr  33969  zarcls  34171  breprexp  34927  bnj168  35026  bnj927  35065  bnj543  35188  bnj970  35242  subfacp1lem6  35535  satfv1  35713  satfvsucsuc  35715  satf0  35722  fmlaomn0  35740  fmla0disjsuc  35748  satffunlem2lem1  35754  mppspstlem  35921  quad3  36020  brdomain  36281  brrange  36282  brimg  36285  brapply  36286  lemsuccf  36289  brfullfun  36298  brrestrict  36299  rankeq1o  36521  sumeq2si  36562  prodeq2si  36564  cbvprodvw2  36607  bj-snsetex  37448  bj-reabeq  37512  bj-rest10  37578  bj-ismooredr2  37600  bj-pinftynminfty  37719  dffinxpf  37879  finxp0  37885  matunitlindflem1  38115  ismblfin  38160  opropabco  38223  fdc  38244  isdrngo1  38455  smprngopr  38551  qseq  39232  eldisjlem19  39412  cdleme25cv  40982  cdlemk35  41536  dicval2  41803  dicopelval2  41805  dicelval2N  41806  hdmap1fval  42420  sn-0tie0  43073  absnw  43260  mzpcompact2lem  43332  eldioph4b  43388  2nn0ind  43522  islmodfg  43646  abeqabi  43984  relintab  44159  brtrclfv2  44303  frege116  44555  elnev  45013  dvnprodlem1  46520  fourierdlem103  46783  fourierdlem104  46784  ovnovollem3  47232  fmtno4prmfac  48181  usgrexmpl2nb1  48654  usgrexmpl2nb2  48655  usgrexmpl2nb3  48656  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  pgnioedg1  48730  pgnioedg2  48731  pgnioedg3  48732  pgnioedg4  48733  pgnioedg5  48734  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem2lem3  48738  pgnbgreunbgrlem5lem1  48742  pgnbgreunbgrlem5lem2  48743  pgnbgreunbgrlem5lem3  48744  lindsrng01  49090  ldepspr  49095  nn0sumshdiglemB  49242  mofeu  49469  f1omo  49514