Theorem eqeq2i 2218

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 2217	. 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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqtri  2228  rabid2  2685  ssalel  3189  equncom  3326  preq12b  3824  preqsn  3829  opeqpr  4316  orddif  4613  dfrel4v  5153  dfiota2  5252  funopg  5324  funopsn  5785  fnressn  5793  fressnfv  5794  acexmidlemph  5960  fnovim  6077  tpossym  6385  qsid  6710  mapsncnv  6805  ixpsnf1o  6846  pw1fin  7033  ss1o0el1o  7036  unfiexmid  7041  onntri35  7383  recidpirq  8006  axprecex  8028  negeq0  8361  muleqadd  8776  fihasheq0  10975  cjne0  11334  sqrt00  11466  sqrtmsq2i  11561  cbvsum  11786  fsump1i  11859  mertenslem2  11962  cbvprod  11984  absefib  12197  efieq1re  12198  isnsg4  13663  plyco  15346  lgsdinn0  15640  m1lgs  15677  upgrex  15814  iswomninnlem  16190