Theorem eqeq2i 2204

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 2203	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtri  2214  rabid2  2671  dfss2  3169  equncom  3305  preq12b  3797  preqsn  3802  opeqpr  4283  orddif  4580  dfrel4v  5118  dfiota2  5217  funopg  5289  fnressn  5745  fressnfv  5746  acexmidlemph  5912  fnovim  6028  tpossym  6331  qsid  6656  mapsncnv  6751  ixpsnf1o  6792  pw1fin  6968  ss1o0el1o  6971  unfiexmid  6976  onntri35  7299  recidpirq  7920  axprecex  7942  negeq0  8275  muleqadd  8689  fihasheq0  10867  cjne0  11055  sqrt00  11187  sqrtmsq2i  11282  cbvsum  11506  fsump1i  11579  mertenslem2  11682  cbvprod  11704  absefib  11917  efieq1re  11918  isnsg4  13285  plyco  14937  lgsdinn0  15205  m1lgs  15242  iswomninnlem  15609