Theorem eqeq2i 2747

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

Syntax hints:   ↔ wb 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  eqeq12i  2752  eqtri  2757  neeq2i  2995  rabid2f  3428  rabid2im  3429  abv  3450  equncom  4109  eq0  4300  ab0w  4329  ab0  4330  ab0orv  4333  absn  4598  rabrsn  4679  ssunpr  4788  sspr  4789  sstp  4790  preq12b  4804  preqsnd  4813  preq12nebg  4817  opthprneg  4819  opeqpr  5451  propssopi  5454  wefrc  5616  dfrel4v  6146  dfrel4  6147  orddif  6413  funopg  6524  f1imadifssran  6576  funcocnv2  6797  dffn5f  6903  fnressn  7101  fressnfv  7103  fnprb  7152  fntpb  7153  riotaeqimp  7339  fnov  7487  ovmpos  7504  onuninsuci  7780  fvresex  7902  elxp6  7965  el2xptp  7977  el2xptp0  7978  opiota  8001  tpossym  8198  qsid  8716  mapsncnv  8829  ixpsnf1o  8874  card1  9878  pm54.43lem  9910  cf0  10159  sdom2en01  10210  cardeq0  10460  enqbreq2  10829  addcompr  10930  mulcompr  10932  axrrecex  11072  negeq0  11433  muleqadd  11779  crne0  12136  dfnn3  12157  xmulneg1  13182  hasheq0  14284  hashbc  14374  hashf1lem2  14377  hash2pwpr  14397  eqwrds3  14882  cjne0  15084  sqrt00  15184  sqrtmsq2i  15309  cbvsum  15616  cbvsumv  15617  fsump1i  15690  cbvprod  15834  cbvprodv  15835  bpoly2  15978  bpoly3  15979  bpoly4  15980  absefib  16121  efieq1re  16122  xpccatid  18109  sgrpidmnd  18662  smndex2dnrinv  18838  isnsg4  19094  opprdomnb  20648  selvval  22076  mat1dimelbas  22413  pmatcollpw3fi1lem1  22728  2ndcctbss  23397  ptcnp  23564  ovolgelb  25435  ioorinv  25531  dvcobr  25903  rolle  25948  dvfsumlem2  25987  plymul0or  26242  reeff1o  26411  sineq0  26487  coseq1  26488  1cubr  26806  atandm2  26841  atandm3  26842  efrlim  26933  efrlimOLD  26934  isppw  27078  ppiub  27169  lgsdinn0  27310  m1lgs  27353  elzs2  28357  elznns  28360  1p1e2s  28374  twocut  28381  uhgr2edg  29230  usgredg2vlem1  29247  usgredg2vlem2  29248  ushgredgedg  29251  ushgredgedgloop  29253  edgnbusgreu  29389  nb3grprlem2  29403  nb3gr2nb  29406  usgredgsscusgredg  29482  usgr2wlkneq  29778  usgr2pthlem  29785  crctcshwlkn0  29843  wwlksn0s  29883  umgr2adedgwlk  29967  umgr2adedgspth  29970  elwwlks2s3  29973  elwwlks2ons3im  29976  rusgrnumwwlkl1  29993  clwlkclwwlkflem  30028  isfrgr  30284  frgr3v  30299  frgrregorufr0  30348  isgrpo  30521  vciOLD  30585  chnlei  31509  h1de2ctlem  31579  cmcmlem  31615  cmcm2i  31617  cmbr2i  31620  osumcor2i  31668  pjss2i  31704  ho01i  31852  nmop0h  32015  pjclem1  32219  jplem1  32292  atabs2i  32426  1arithidom  33567  ply1dg1rt  33610  vieta  33685  fedgmullem2  33736  ccfldextdgrr  33778  zarcls  33980  breprexp  34739  bnj168  34835  bnj927  34874  bnj543  34998  bnj970  35052  subfacp1lem6  35328  satfv1  35506  satfvsucsuc  35508  satf0  35515  fmlaomn0  35533  fmla0disjsuc  35541  satffunlem2lem1  35547  mppspstlem  35714  quad3  35813  brdomain  36074  brrange  36075  brimg  36078  brapply  36079  lemsuccf  36082  brfullfun  36091  brrestrict  36092  rankeq1o  36314  sumeq2si  36345  prodeq2si  36347  cbvprodvw2  36390  bj-snsetex  37107  bj-reabeq  37171  bj-rest10  37232  bj-ismooredr2  37254  bj-pinftynminfty  37371  dffinxpf  37529  finxp0  37535  matunitlindflem1  37756  ismblfin  37801  opropabco  37864  fdc  37885  isdrngo1  38096  smprngopr  38192  qseq  38846  eldisjlem19  39008  cdleme25cv  40557  cdlemk35  41111  dicval2  41378  dicopelval2  41380  dicelval2N  41381  hdmap1fval  41995  sn-0tie0  42648  absnw  42863  mzpcompact2lem  42935  eldioph4b  42995  2nn0ind  43129  islmodfg  43253  abeqabi  43591  relintab  43766  brtrclfv2  43910  frege116  44162  elnev  44620  dvnprodlem1  46132  fourierdlem103  46395  fourierdlem104  46396  ovnovollem3  46844  fmtno4prmfac  47760  usgrexmpl2nb1  48220  usgrexmpl2nb2  48221  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  pgnioedg1  48296  pgnioedg2  48297  pgnioedg3  48298  pgnioedg4  48299  pgnioedg5  48300  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  pgnbgreunbgrlem5lem1  48308  pgnbgreunbgrlem5lem2  48309  pgnbgreunbgrlem5lem3  48310  lindsrng01  48656  ldepspr  48661  nn0sumshdiglemB  48808  mofeu  49035  f1omo  49080