Theorem eqeq2i 2207

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

Syntax hints:   <-> wb 105   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtri  2217  rabid2  2674  ssalel  3172  equncom  3309  preq12b  3801  preqsn  3806  opeqpr  4287  orddif  4584  dfrel4v  5122  dfiota2  5221  funopg  5293  fnressn  5751  fressnfv  5752  acexmidlemph  5918  fnovim  6035  tpossym  6343  qsid  6668  mapsncnv  6763  ixpsnf1o  6804  pw1fin  6980  ss1o0el1o  6983  unfiexmid  6988  onntri35  7320  recidpirq  7942  axprecex  7964  negeq0  8297  muleqadd  8712  fihasheq0  10902  cjne0  11090  sqrt00  11222  sqrtmsq2i  11317  cbvsum  11542  fsump1i  11615  mertenslem2  11718  cbvprod  11740  absefib  11953  efieq1re  11954  isnsg4  13418  plyco  15079  lgsdinn0  15373  m1lgs  15410  iswomninnlem  15780