Theorem eqeq2i 2242

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

Syntax hints:   <-> wb 105   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqtri  2252  rabid2  2711  ssalel  3216  equncom  3354  preq12b  3858  preqsn  3863  opeqpr  4352  orddif  4651  dfrel4v  5195  dfiota2  5294  funopg  5367  funopsn  5838  fnressn  5848  fressnfv  5849  riotaeqimp  6006  acexmidlemph  6021  fnovim  6140  tpossym  6485  qsid  6812  mapsncnv  6907  ixpsnf1o  6948  pw1fin  7145  ss1o0el1o  7148  unfiexmid  7153  onntri35  7515  recidpirq  8138  axprecex  8160  negeq0  8492  muleqadd  8907  fihasheq0  11118  cjne0  11548  sqrt00  11680  sqrtmsq2i  11775  cbvsum  12000  fsump1i  12074  mertenslem2  12177  cbvprod  12199  absefib  12412  efieq1re  12413  isnsg4  13879  plyco  15570  lgsdinn0  15867  m1lgs  15904  upgrex  16044  uhgr2edg  16147  usgredg2vlem1  16163  usgredg2vlem2  16164  ushgredgedg  16167  ushgredgedgloop  16169  exmidnotnotr  16727  iswomninnlem  16782