Theorem eqeq2i 2125

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

Syntax hints:   <-> wb 104   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  eqtri  2135  rabid2  2581  dfss2  3052  equncom  3187  preq12b  3663  preqsn  3668  opeqpr  4135  orddif  4422  dfrel4v  4948  dfiota2  5047  funopg  5115  fnressn  5560  fressnfv  5561  acexmidlemph  5721  fnovim  5833  tpossym  6127  qsid  6448  mapsncnv  6543  ixpsnf1o  6584  unfiexmid  6759  recidpirq  7593  axprecex  7615  negeq0  7939  muleqadd  8342  fihasheq0  10433  cjne0  10573  sqrt00  10704  sqrtmsq2i  10799  cbvsum  11021  fsump1i  11094  mertenslem2  11197  absefib  11327  efieq1re  11328