Theorem eqeq2i 2240

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

Syntax hints:   <-> wb 105   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtri  2250  rabid2  2708  ssalel  3212  equncom  3349  preq12b  3848  preqsn  3853  opeqpr  4340  orddif  4639  dfrel4v  5180  dfiota2  5279  funopg  5352  funopsn  5819  fnressn  5829  fressnfv  5830  riotaeqimp  5985  acexmidlemph  6000  fnovim  6119  tpossym  6428  qsid  6755  mapsncnv  6850  ixpsnf1o  6891  pw1fin  7083  ss1o0el1o  7086  unfiexmid  7091  onntri35  7433  recidpirq  8056  axprecex  8078  negeq0  8411  muleqadd  8826  fihasheq0  11027  cjne0  11435  sqrt00  11567  sqrtmsq2i  11662  cbvsum  11887  fsump1i  11960  mertenslem2  12063  cbvprod  12085  absefib  12298  efieq1re  12299  isnsg4  13765  plyco  15449  lgsdinn0  15743  m1lgs  15780  upgrex  15919  uhgr2edg  16020  usgredg2vlem1  16036  usgredg2vlem2  16037  ushgredgedg  16040  ushgredgedgloop  16042  iswomninnlem  16505