Theorem eqeq2i 2216

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

Syntax hints:   <-> wb 105   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqtri  2226  rabid2  2683  ssalel  3181  equncom  3318  preq12b  3811  preqsn  3816  opeqpr  4299  orddif  4596  dfrel4v  5135  dfiota2  5234  funopg  5306  funopsn  5764  fnressn  5772  fressnfv  5773  acexmidlemph  5939  fnovim  6056  tpossym  6364  qsid  6689  mapsncnv  6784  ixpsnf1o  6825  pw1fin  7009  ss1o0el1o  7012  unfiexmid  7017  onntri35  7351  recidpirq  7973  axprecex  7995  negeq0  8328  muleqadd  8743  fihasheq0  10940  cjne0  11252  sqrt00  11384  sqrtmsq2i  11479  cbvsum  11704  fsump1i  11777  mertenslem2  11880  cbvprod  11902  absefib  12115  efieq1re  12116  isnsg4  13581  plyco  15264  lgsdinn0  15558  m1lgs  15595  iswomninnlem  16025