Theorem eqeq2i 2216

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 2215	. 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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqtri  2226  rabid2  2683  ssalel  3181  equncom  3318  preq12b  3811  preqsn  3816  opeqpr  4298  orddif  4595  dfrel4v  5134  dfiota2  5233  funopg  5305  funopsn  5762  fnressn  5770  fressnfv  5771  acexmidlemph  5937  fnovim  6054  tpossym  6362  qsid  6687  mapsncnv  6782  ixpsnf1o  6823  pw1fin  7007  ss1o0el1o  7010  unfiexmid  7015  onntri35  7349  recidpirq  7971  axprecex  7993  negeq0  8326  muleqadd  8741  fihasheq0  10938  cjne0  11219  sqrt00  11351  sqrtmsq2i  11446  cbvsum  11671  fsump1i  11744  mertenslem2  11847  cbvprod  11869  absefib  12082  efieq1re  12083  isnsg4  13548  plyco  15231  lgsdinn0  15525  m1lgs  15562  iswomninnlem  15992