Theorem eqeq2i 2148

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 2147	. 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 2119

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

This theorem is referenced by:  eqtri  2158  rabid2  2605  dfss2  3081  equncom  3216  preq12b  3692  preqsn  3697  opeqpr  4170  orddif  4457  dfrel4v  4985  dfiota2  5084  funopg  5152  fnressn  5599  fressnfv  5600  acexmidlemph  5760  fnovim  5872  tpossym  6166  qsid  6487  mapsncnv  6582  ixpsnf1o  6623  unfiexmid  6799  recidpirq  7659  axprecex  7681  negeq0  8009  muleqadd  8422  fihasheq0  10533  cjne0  10673  sqrt00  10805  sqrtmsq2i  10900  cbvsum  11122  fsump1i  11195  mertenslem2  11298  cbvprod  11320  absefib  11466  efieq1re  11467