Theorem eqeq2i 2750

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 2749	. 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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  eqeq12i  2755  eqtri  2765  neeq2i  3006  rabid2f  3468  rabid2im  3469  rabid2OLD  3471  abv  3492  equncom  4159  eq0  4350  ab0w  4379  ab0  4380  ab0orv  4383  eq0rdv  4407  rzal  4509  absn  4645  rabrsn  4724  ssunpr  4834  sspr  4835  sstp  4836  preq12b  4850  preqsnd  4859  preq12nebg  4863  opthprneg  4865  opeqpr  5510  propssopi  5513  wefrc  5679  dfrel4v  6210  dfrel4  6211  orddif  6480  funopg  6600  f1imadifssran  6652  funimaexgOLD  6654  funcocnv2  6873  dffn5f  6980  fnressn  7178  fressnfv  7180  fnprb  7228  fntpb  7229  riotaeqimp  7414  fnov  7564  ovmpos  7581  onuninsuci  7861  fvresex  7984  elxp6  8048  el2xptp  8060  el2xptp0  8061  opiota  8084  tpossym  8283  dfwrecsOLD  8338  qsid  8823  mapsncnv  8933  ixpsnf1o  8978  card1  10008  pm54.43lem  10040  cf0  10291  sdom2en01  10342  cardeq0  10592  enqbreq2  10960  addcompr  11061  mulcompr  11063  axrrecex  11203  negeq0  11563  muleqadd  11907  crne0  12259  dfnn3  12280  xmulneg1  13311  hasheq0  14402  hashbc  14492  hashf1lem2  14495  hash2pwpr  14515  eqwrds3  15000  cjne0  15202  sqrt00  15302  sqrtmsq2i  15426  cbvsum  15731  cbvsumv  15732  fsump1i  15805  cbvprod  15949  cbvprodv  15950  bpoly2  16093  bpoly3  16094  bpoly4  16095  absefib  16234  efieq1re  16235  xpccatid  18233  sgrpidmnd  18752  smndex2dnrinv  18928  isnsg4  19185  opprdomnb  20717  selvval  22139  mat1dimelbas  22477  pmatcollpw3fi1lem1  22792  2ndcctbss  23463  ptcnp  23630  ovolgelb  25515  ioorinv  25611  dvcobr  25983  rolle  26028  dvfsumlem2  26067  plymul0or  26322  reeff1o  26491  sineq0  26566  coseq1  26567  1cubr  26885  atandm2  26920  atandm3  26921  efrlim  27012  efrlimOLD  27013  isppw  27157  ppiub  27248  lgsdinn0  27389  m1lgs  27432  elzs2  28385  elznns  28388  1p1e2s  28400  uhgr2edg  29225  usgredg2vlem1  29242  usgredg2vlem2  29243  ushgredgedg  29246  ushgredgedgloop  29248  edgnbusgreu  29384  nb3grprlem2  29398  nb3gr2nb  29401  usgredgsscusgredg  29477  usgr2wlkneq  29776  usgr2pthlem  29783  crctcshwlkn0  29841  wwlksn0s  29881  umgr2adedgwlk  29965  umgr2adedgspth  29968  elwwlks2s3  29971  elwwlks2ons3im  29974  rusgrnumwwlkl1  29988  clwlkclwwlkflem  30023  isfrgr  30279  frgr3v  30294  frgrregorufr0  30343  isgrpo  30516  vciOLD  30580  chnlei  31504  h1de2ctlem  31574  cmcmlem  31610  cmcm2i  31612  cmbr2i  31615  osumcor2i  31663  pjss2i  31699  ho01i  31847  nmop0h  32010  pjclem1  32214  jplem1  32287  atabs2i  32421  1arithidom  33565  ply1dg1rt  33604  fedgmullem2  33681  ccfldextdgrr  33722  zarcls  33873  breprexp  34648  bnj168  34744  bnj927  34783  bnj543  34907  bnj970  34961  subfacp1lem6  35190  satfv1  35368  satfvsucsuc  35370  satf0  35377  fmlaomn0  35395  fmla0disjsuc  35403  satffunlem2lem1  35409  mppspstlem  35576  quad3  35675  brdomain  35934  brrange  35935  brimg  35938  brapply  35939  brsuccf  35942  brfullfun  35949  brrestrict  35950  rankeq1o  36172  sumeq2si  36203  prodeq2si  36205  cbvprodvw2  36248  bj-snsetex  36964  bj-reabeq  37028  bj-rest10  37089  bj-ismooredr2  37111  bj-pinftynminfty  37228  dffinxpf  37386  finxp0  37392  matunitlindflem1  37623  ismblfin  37668  opropabco  37731  fdc  37752  isdrngo1  37963  smprngopr  38059  eldisjlem19  38811  cdleme25cv  40360  cdlemk35  40914  dicval2  41181  dicopelval2  41183  dicelval2N  41184  hdmap1fval  41798  sn-0tie0  42469  absnw  42688  mzpcompact2lem  42762  eldioph4b  42822  2nn0ind  42957  islmodfg  43081  abeqabi  43421  relintab  43596  brtrclfv2  43740  frege116  43992  elnev  44457  dvnprodlem1  45961  fourierdlem103  46224  fourierdlem104  46225  ovnovollem3  46673  fmtno4prmfac  47559  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  lindsrng01  48385  ldepspr  48390  nn0sumshdiglemB  48541  mofeu  48757