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  5817  fnressn  5825  fressnfv  5826  riotaeqimp  5979  acexmidlemph  5994  fnovim  6113  tpossym  6422  qsid  6747  mapsncnv  6842  ixpsnf1o  6883  pw1fin  7072  ss1o0el1o  7075  unfiexmid  7080  onntri35  7422  recidpirq  8045  axprecex  8067  negeq0  8400  muleqadd  8815  fihasheq0  11015  cjne0  11419  sqrt00  11551  sqrtmsq2i  11646  cbvsum  11871  fsump1i  11944  mertenslem2  12047  cbvprod  12069  absefib  12282  efieq1re  12283  isnsg4  13749  plyco  15433  lgsdinn0  15727  m1lgs  15764  upgrex  15903  uhgr2edg  16004  usgredg2vlem1  16020  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  iswomninnlem  16417