Theorem eqeq2i 2150

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

Syntax hints:   <-> wb 104   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  eqtri  2160  rabid2  2607  dfss2  3086  equncom  3221  preq12b  3697  preqsn  3702  opeqpr  4175  orddif  4462  dfrel4v  4990  dfiota2  5089  funopg  5157  fnressn  5606  fressnfv  5607  acexmidlemph  5767  fnovim  5879  tpossym  6173  qsid  6494  mapsncnv  6589  ixpsnf1o  6630  unfiexmid  6806  recidpirq  7666  axprecex  7688  negeq0  8016  muleqadd  8429  fihasheq0  10540  cjne0  10680  sqrt00  10812  sqrtmsq2i  10907  cbvsum  11129  fsump1i  11202  mertenslem2  11305  cbvprod  11327  absefib  11477  efieq1re  11478