Theorem eqeq2i 2186

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

Syntax hints:   <-> wb 105   = wceq 1353

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  eqtri  2196  rabid2  2651  dfss2  3142  equncom  3278  preq12b  3766  preqsn  3771  opeqpr  4247  orddif  4540  dfrel4v  5072  dfiota2  5171  funopg  5242  fnressn  5694  fressnfv  5695  acexmidlemph  5858  fnovim  5973  tpossym  6267  qsid  6590  mapsncnv  6685  ixpsnf1o  6726  pw1fin  6900  ss1o0el1o  6902  unfiexmid  6907  onntri35  7226  recidpirq  7832  axprecex  7854  negeq0  8185  muleqadd  8598  fihasheq0  10739  cjne0  10883  sqrt00  11015  sqrtmsq2i  11110  cbvsum  11334  fsump1i  11407  mertenslem2  11510  cbvprod  11532  absefib  11744  efieq1re  11745  lgsdinn0  14018  iswomninnlem  14356