Theorem eqeq2i 2742

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 2741	. 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  eqtri  2752  neeq2i  2990  rabid2f  3437  rabid2im  3438  abv  3459  equncom  4122  eq0  4313  ab0w  4342  ab0  4343  ab0orv  4346  eq0rdv  4370  rzal  4472  absn  4609  rabrsn  4688  ssunpr  4798  sspr  4799  sstp  4800  preq12b  4814  preqsnd  4823  preq12nebg  4827  opthprneg  4829  opeqpr  5465  propssopi  5468  wefrc  5632  dfrel4v  6163  dfrel4  6164  orddif  6430  funopg  6550  f1imadifssran  6602  funimaexgOLD  6604  funcocnv2  6825  dffn5f  6932  fnressn  7130  fressnfv  7132  fnprb  7182  fntpb  7183  riotaeqimp  7370  fnov  7520  ovmpos  7537  onuninsuci  7816  fvresex  7938  elxp6  8002  el2xptp  8014  el2xptp0  8015  opiota  8038  tpossym  8237  qsid  8754  mapsncnv  8866  ixpsnf1o  8911  card1  9921  pm54.43lem  9953  cf0  10204  sdom2en01  10255  cardeq0  10505  enqbreq2  10873  addcompr  10974  mulcompr  10976  axrrecex  11116  negeq0  11476  muleqadd  11822  crne0  12179  dfnn3  12200  xmulneg1  13229  hasheq0  14328  hashbc  14418  hashf1lem2  14421  hash2pwpr  14441  eqwrds3  14927  cjne0  15129  sqrt00  15229  sqrtmsq2i  15354  cbvsum  15661  cbvsumv  15662  fsump1i  15735  cbvprod  15879  cbvprodv  15880  bpoly2  16023  bpoly3  16024  bpoly4  16025  absefib  16166  efieq1re  16167  xpccatid  18149  sgrpidmnd  18666  smndex2dnrinv  18842  isnsg4  19099  opprdomnb  20626  selvval  22022  mat1dimelbas  22358  pmatcollpw3fi1lem1  22673  2ndcctbss  23342  ptcnp  23509  ovolgelb  25381  ioorinv  25477  dvcobr  25849  rolle  25894  dvfsumlem2  25933  plymul0or  26188  reeff1o  26357  sineq0  26433  coseq1  26434  1cubr  26752  atandm2  26787  atandm3  26788  efrlim  26879  efrlimOLD  26880  isppw  27024  ppiub  27115  lgsdinn0  27256  m1lgs  27299  elzs2  28287  elznns  28290  1p1e2s  28302  twocut  28309  uhgr2edg  29135  usgredg2vlem1  29152  usgredg2vlem2  29153  ushgredgedg  29156  ushgredgedgloop  29158  edgnbusgreu  29294  nb3grprlem2  29308  nb3gr2nb  29311  usgredgsscusgredg  29387  usgr2wlkneq  29686  usgr2pthlem  29693  crctcshwlkn0  29751  wwlksn0s  29791  umgr2adedgwlk  29875  umgr2adedgspth  29878  elwwlks2s3  29881  elwwlks2ons3im  29884  rusgrnumwwlkl1  29898  clwlkclwwlkflem  29933  isfrgr  30189  frgr3v  30204  frgrregorufr0  30253  isgrpo  30426  vciOLD  30490  chnlei  31414  h1de2ctlem  31484  cmcmlem  31520  cmcm2i  31522  cmbr2i  31525  osumcor2i  31573  pjss2i  31609  ho01i  31757  nmop0h  31920  pjclem1  32124  jplem1  32197  atabs2i  32331  1arithidom  33508  ply1dg1rt  33548  fedgmullem2  33626  ccfldextdgrr  33667  zarcls  33864  breprexp  34624  bnj168  34720  bnj927  34759  bnj543  34883  bnj970  34937  subfacp1lem6  35172  satfv1  35350  satfvsucsuc  35352  satf0  35359  fmlaomn0  35377  fmla0disjsuc  35385  satffunlem2lem1  35391  mppspstlem  35558  quad3  35657  brdomain  35921  brrange  35922  brimg  35925  brapply  35926  brsuccf  35929  brfullfun  35936  brrestrict  35937  rankeq1o  36159  sumeq2si  36190  prodeq2si  36192  cbvprodvw2  36235  bj-snsetex  36951  bj-reabeq  37015  bj-rest10  37076  bj-ismooredr2  37098  bj-pinftynminfty  37215  dffinxpf  37373  finxp0  37379  matunitlindflem1  37610  ismblfin  37655  opropabco  37718  fdc  37739  isdrngo1  37950  smprngopr  38046  qseq  38640  eldisjlem19  38802  cdleme25cv  40352  cdlemk35  40906  dicval2  41173  dicopelval2  41175  dicelval2N  41176  hdmap1fval  41790  sn-0tie0  42439  absnw  42666  mzpcompact2lem  42739  eldioph4b  42799  2nn0ind  42934  islmodfg  43058  abeqabi  43397  relintab  43572  brtrclfv2  43716  frege116  43968  elnev  44427  dvnprodlem1  45944  fourierdlem103  46207  fourierdlem104  46208  ovnovollem3  46656  fmtno4prmfac  47573  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  lindsrng01  48457  ldepspr  48462  nn0sumshdiglemB  48609  mofeu  48836  f1omo  48881