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  3426  rabid2im  3427  abv  3448  equncom  4110  eq0  4301  ab0w  4330  ab0  4331  ab0orv  4334  eq0rdv  4358  rzal  4460  absn  4597  rabrsn  4676  ssunpr  4785  sspr  4786  sstp  4787  preq12b  4801  preqsnd  4810  preq12nebg  4814  opthprneg  4816  opeqpr  5448  propssopi  5451  wefrc  5613  dfrel4v  6139  dfrel4  6140  orddif  6405  funopg  6516  f1imadifssran  6568  funcocnv2  6789  dffn5f  6894  fnressn  7092  fressnfv  7094  fnprb  7144  fntpb  7145  riotaeqimp  7332  fnov  7480  ovmpos  7497  onuninsuci  7773  fvresex  7895  elxp6  7958  el2xptp  7970  el2xptp0  7971  opiota  7994  tpossym  8191  qsid  8708  mapsncnv  8820  ixpsnf1o  8865  card1  9864  pm54.43lem  9896  cf0  10145  sdom2en01  10196  cardeq0  10446  enqbreq2  10814  addcompr  10915  mulcompr  10917  axrrecex  11057  negeq0  11418  muleqadd  11764  crne0  12121  dfnn3  12142  xmulneg1  13171  hasheq0  14270  hashbc  14360  hashf1lem2  14363  hash2pwpr  14383  eqwrds3  14868  cjne0  15070  sqrt00  15170  sqrtmsq2i  15295  cbvsum  15602  cbvsumv  15603  fsump1i  15676  cbvprod  15820  cbvprodv  15821  bpoly2  15964  bpoly3  15965  bpoly4  15966  absefib  16107  efieq1re  16108  xpccatid  18094  sgrpidmnd  18613  smndex2dnrinv  18789  isnsg4  19046  opprdomnb  20602  selvval  22020  mat1dimelbas  22356  pmatcollpw3fi1lem1  22671  2ndcctbss  23340  ptcnp  23507  ovolgelb  25379  ioorinv  25475  dvcobr  25847  rolle  25892  dvfsumlem2  25931  plymul0or  26186  reeff1o  26355  sineq0  26431  coseq1  26432  1cubr  26750  atandm2  26785  atandm3  26786  efrlim  26877  efrlimOLD  26878  isppw  27022  ppiub  27113  lgsdinn0  27254  m1lgs  27297  elzs2  28292  elznns  28295  1p1e2s  28308  twocut  28315  uhgr2edg  29153  usgredg2vlem1  29170  usgredg2vlem2  29171  ushgredgedg  29174  ushgredgedgloop  29176  edgnbusgreu  29312  nb3grprlem2  29326  nb3gr2nb  29329  usgredgsscusgredg  29405  usgr2wlkneq  29701  usgr2pthlem  29708  crctcshwlkn0  29766  wwlksn0s  29806  umgr2adedgwlk  29890  umgr2adedgspth  29893  elwwlks2s3  29896  elwwlks2ons3im  29899  rusgrnumwwlkl1  29913  clwlkclwwlkflem  29948  isfrgr  30204  frgr3v  30219  frgrregorufr0  30268  isgrpo  30441  vciOLD  30505  chnlei  31429  h1de2ctlem  31499  cmcmlem  31535  cmcm2i  31537  cmbr2i  31540  osumcor2i  31588  pjss2i  31624  ho01i  31772  nmop0h  31935  pjclem1  32139  jplem1  32212  atabs2i  32346  1arithidom  33474  ply1dg1rt  33515  fedgmullem2  33597  ccfldextdgrr  33639  zarcls  33841  breprexp  34601  bnj168  34697  bnj927  34736  bnj543  34860  bnj970  34914  subfacp1lem6  35158  satfv1  35336  satfvsucsuc  35338  satf0  35345  fmlaomn0  35363  fmla0disjsuc  35371  satffunlem2lem1  35377  mppspstlem  35544  quad3  35643  brdomain  35907  brrange  35908  brimg  35911  brapply  35912  brsuccf  35915  brfullfun  35922  brrestrict  35923  rankeq1o  36145  sumeq2si  36176  prodeq2si  36178  cbvprodvw2  36221  bj-snsetex  36937  bj-reabeq  37001  bj-rest10  37062  bj-ismooredr2  37084  bj-pinftynminfty  37201  dffinxpf  37359  finxp0  37365  matunitlindflem1  37596  ismblfin  37641  opropabco  37704  fdc  37725  isdrngo1  37936  smprngopr  38032  qseq  38626  eldisjlem19  38788  cdleme25cv  40337  cdlemk35  40891  dicval2  41158  dicopelval2  41160  dicelval2N  41161  hdmap1fval  41775  sn-0tie0  42424  absnw  42651  mzpcompact2lem  42724  eldioph4b  42784  2nn0ind  42918  islmodfg  43042  abeqabi  43381  relintab  43556  brtrclfv2  43700  frege116  43952  elnev  44411  dvnprodlem1  45927  fourierdlem103  46190  fourierdlem104  46191  ovnovollem3  46639  fmtno4prmfac  47556  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  pgnioedg1  48092  pgnioedg2  48093  pgnioedg3  48094  pgnioedg4  48095  pgnioedg5  48096  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  pgnbgreunbgrlem5lem1  48104  pgnbgreunbgrlem5lem2  48105  pgnbgreunbgrlem5lem3  48106  lindsrng01  48453  ldepspr  48458  nn0sumshdiglemB  48605  mofeu  48832  f1omo  48877