Theorem eqeq2i 2414

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	|- A = B

Assertion

Ref	Expression
eqeq2i	|- ( C = A <-> C = B )

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 |- A = B
2		eqeq2 2413	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	ax-mp 8	1 |- ( C = A <-> C = B )

Syntax hints:   <-> wb 177   = wceq 1649

This theorem is referenced by:  eqtri  2424  rabid2  2845  dfss2  3297  equncom  3452  ssunpr  3921  sspr  3922  sstp  3923  preq12b  3934  preqsn  3940  opeqpr  4413  wefrc  4536  orddif  4634  onuninsuci  4779  dfrel4v  5281  dfiota2  5378  funopg  5444  funimaexg  5489  dffn5f  5740  fnressn  5877  fressnfv  5879  fvresex  5941  fnov  6137  elxp6  6337  tpossym  6470  opiota  6494  qsid  6929  mapsncnv  7019  ixpsnf1o  7061  card1  7811  pm54.43lem  7842  cf0  8087  sdom2en01  8138  cardeq0  8383  enqbreq2  8753  addcompr  8854  mulcompr  8856  axrrecex  8994  negeq0  9311  muleqadd  9622  crne0  9949  dfnn3  9970  xmulneg1  10804  hasheq0  11599  hashbc  11657  hashf1lem2  11660  cjne0  11923  sqr00  12024  sqrmsq2i  12146  fsump1i  12508  absefib  12754  efieq1re  12755  xpccatid  14240  isnsg4  14938  2ndcctbss  17471  ptcnp  17607  ovolgelb  19329  ioorinv  19421  rolle  19827  plymul0or  20151  reeff1o  20316  sineq0  20382  coseq1  20383  1cubr  20635  atandm2  20670  atandm3  20671  efrlim  20761  isppw  20850  ppiub  20941  lgsdinn0  21077  m1lgs  21099  usgra2edg  21355  usgraedg4  21359  usgraidx2vlem1  21363  usgraidx2vlem2  21364  nb3graprlem2  21414  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  2trllemH  21505  2trllemE  21506  usgrcyclnl2  21581  4cycl4dv  21607  isgrpo  21737  vci  21980  chnlei  22940  h1de2ctlem  23010  cmcmlem  23046  cmcm2i  23048  cmbr2i  23051  osumcor2i  23099  pjss2i  23135  ho01i  23284  nmop0h  23447  pjclem1  23651  jplem1  23724  atabs2i  23858  rabid2f  23920  preqsnd  23953  dfrel4  23987  subfacp1lem6  24824  cbvprod  25194  trpredmintr  25448  brdomain  25686  brrange  25687  brimg  25690  brapply  25691  brsuccf  25694  brfullfun  25701  brrestrict  25702  bpoly2  26007  bpoly3  26008  bpoly4  26009  rankeq1o  26016  ismblfin  26146  opropabco  26315  fdc  26339  isdrngo1  26462  smprngopr  26552  mzpcompact2lem  26698  eldioph4b  26762  2nn0ind  26898  islmodfg  27035  elnev  27506  el2xptp  27948  el2xptp0  27949  euhash1  27998  usgra2pthlem1  28040  2pthfrgra  28115  bnj168  28803  bnj927  28845  bnj543  28970  bnj970  29024  cdleme25cv  30840  cdlemk35  31394  dicval2  31662  dicopelval2  31664  dicelval2N  31665  hdmap1fval  32280

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397