Theorem eqeq2i 2743

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

Syntax hints:   ↔ wb 205   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeq12i  2748  eqtri  2758  neeq2i  3004  rabid2f  3461  rabid2OLD  3463  abv  3483  dfss2OLD  3968  equncom  4153  eq0  4342  ab0w  4372  ab0  4373  ab0OLD  4374  ab0orv  4377  eq0rdv  4403  rzal  4507  absn  4645  rabrsn  4727  ssunpr  4834  sspr  4835  sstp  4836  preq12b  4850  preqsnd  4858  preq12nebg  4862  opthprneg  4864  opeqpr  5504  propssopi  5507  wefrc  5669  dfrel4v  6188  dfrel4  6189  orddif  6459  funopg  6581  funimaexgOLD  6634  funcocnv2  6857  dffn5f  6962  fnressn  7157  fressnfv  7159  fnprb  7211  fntpb  7212  riotaeqimp  7394  fnov  7542  ovmpos  7558  onuninsuci  7831  fvresex  7948  elxp6  8011  el2xptp  8023  el2xptp0  8024  opiota  8047  tpossym  8245  dfwrecsOLD  8300  qsid  8779  mapsncnv  8889  ixpsnf1o  8934  card1  9965  pm54.43lem  9997  cf0  10248  sdom2en01  10299  cardeq0  10549  enqbreq2  10917  addcompr  11018  mulcompr  11020  axrrecex  11160  negeq0  11518  muleqadd  11862  crne0  12209  dfnn3  12230  xmulneg1  13252  hasheq0  14327  hashbc  14416  hashf1lem2  14421  hash2pwpr  14441  eqwrds3  14916  cjne0  15114  sqrt00  15214  sqrtmsq2i  15338  cbvsum  15645  fsump1i  15719  cbvprod  15863  bpoly2  16005  bpoly3  16006  bpoly4  16007  absefib  16145  efieq1re  16146  xpccatid  18144  sgrpidmnd  18664  smndex2dnrinv  18832  isnsg4  19083  selvval  21900  mat1dimelbas  22193  pmatcollpw3fi1lem1  22508  2ndcctbss  23179  ptcnp  23346  ovolgelb  25229  ioorinv  25325  dvcobr  25697  rolle  25742  plymul0or  26030  reeff1o  26195  sineq0  26269  coseq1  26270  1cubr  26583  atandm2  26618  atandm3  26619  efrlim  26710  isppw  26854  ppiub  26943  lgsdinn0  27084  m1lgs  27127  uhgr2edg  28732  usgredg2vlem1  28749  usgredg2vlem2  28750  ushgredgedg  28753  ushgredgedgloop  28755  edgnbusgreu  28891  nb3grprlem2  28905  nb3gr2nb  28908  usgredgsscusgredg  28983  usgr2wlkneq  29280  usgr2pthlem  29287  crctcshwlkn0  29342  wwlksn0s  29382  umgr2adedgwlk  29466  umgr2adedgspth  29469  elwwlks2s3  29472  elwwlks2ons3im  29475  rusgrnumwwlkl1  29489  clwlkclwwlkflem  29524  isfrgr  29780  frgr3v  29795  frgrregorufr0  29844  isgrpo  30017  vciOLD  30081  chnlei  31005  h1de2ctlem  31075  cmcmlem  31111  cmcm2i  31113  cmbr2i  31116  osumcor2i  31164  pjss2i  31200  ho01i  31348  nmop0h  31511  pjclem1  31715  jplem1  31788  atabs2i  31922  fedgmullem2  33003  ccfldextdgrr  33035  zarcls  33152  breprexp  33943  bnj168  34039  bnj927  34078  bnj543  34202  bnj970  34256  subfacp1lem6  34474  satfv1  34652  satfvsucsuc  34654  satf0  34661  fmlaomn0  34679  fmla0disjsuc  34687  satffunlem2lem1  34693  mppspstlem  34860  quad3  34953  brdomain  35209  brrange  35210  brimg  35213  brapply  35214  brsuccf  35217  brfullfun  35224  brrestrict  35225  rankeq1o  35447  gg-dvfsumlem2  35469  bj-snsetex  36147  bj-reabeq  36211  bj-rest10  36272  bj-ismooredr2  36294  bj-pinftynminfty  36411  dffinxpf  36569  finxp0  36575  matunitlindflem1  36787  ismblfin  36832  opropabco  36895  fdc  36916  isdrngo1  37127  smprngopr  37223  eldisjlem19  37983  cdleme25cv  39532  cdlemk35  40086  dicval2  40353  dicopelval2  40355  dicelval2N  40356  hdmap1fval  40970  sn-0tie0  41614  mzpcompact2lem  41791  eldioph4b  41851  2nn0ind  41986  islmodfg  42113  abeqabi  42461  relintab  42636  brtrclfv2  42780  frege116  43032  elnev  43499  dvnprodlem1  44960  fourierdlem103  45223  fourierdlem104  45224  ovnovollem3  45672  fmtno4prmfac  46538  lindsrng01  47236  ldepspr  47241  nn0sumshdiglemB  47393  mofeu  47601