Theorem eqeq2i 2242

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 2241	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	ax-mp 5	1 |- ( C = A <-> C = B )

Syntax hints:   <-> wb 105   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqtri  2252  rabid2  2710  ssalel  3215  equncom  3352  preq12b  3853  preqsn  3858  opeqpr  4346  orddif  4645  dfrel4v  5188  dfiota2  5287  funopg  5360  funopsn  5830  fnressn  5840  fressnfv  5841  riotaeqimp  5996  acexmidlemph  6011  fnovim  6130  tpossym  6442  qsid  6769  mapsncnv  6864  ixpsnf1o  6905  pw1fin  7102  ss1o0el1o  7105  unfiexmid  7110  onntri35  7455  recidpirq  8078  axprecex  8100  negeq0  8433  muleqadd  8848  fihasheq0  11056  cjne0  11486  sqrt00  11618  sqrtmsq2i  11713  cbvsum  11938  fsump1i  12012  mertenslem2  12115  cbvprod  12137  absefib  12350  efieq1re  12351  isnsg4  13817  plyco  15502  lgsdinn0  15796  m1lgs  15833  upgrex  15973  uhgr2edg  16076  usgredg2vlem1  16092  usgredg2vlem2  16093  ushgredgedg  16096  ushgredgedgloop  16098  iswomninnlem  16705