Theorem eqeq2i 2207

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq2i	⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq2 2206	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 105   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtri  2217  rabid2  2674  ssalel  3172  equncom  3309  preq12b  3801  preqsn  3806  opeqpr  4287  orddif  4584  dfrel4v  5122  dfiota2  5221  funopg  5293  fnressn  5751  fressnfv  5752  acexmidlemph  5918  fnovim  6035  tpossym  6343  qsid  6668  mapsncnv  6763  ixpsnf1o  6804  pw1fin  6980  ss1o0el1o  6983  unfiexmid  6988  onntri35  7322  recidpirq  7944  axprecex  7966  negeq0  8299  muleqadd  8714  fihasheq0  10904  cjne0  11092  sqrt00  11224  sqrtmsq2i  11319  cbvsum  11544  fsump1i  11617  mertenslem2  11720  cbvprod  11742  absefib  11955  efieq1re  11956  isnsg4  13420  plyco  15103  lgsdinn0  15397  m1lgs  15434  iswomninnlem  15806