Theorem eqeq2i 2176

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 2175	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 104   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqtri  2186  rabid2  2642  dfss2  3131  equncom  3267  preq12b  3750  preqsn  3755  opeqpr  4231  orddif  4524  dfrel4v  5055  dfiota2  5154  funopg  5222  fnressn  5671  fressnfv  5672  acexmidlemph  5835  fnovim  5950  tpossym  6244  qsid  6566  mapsncnv  6661  ixpsnf1o  6702  pw1fin  6876  ss1o0el1o  6878  unfiexmid  6883  onntri35  7193  recidpirq  7799  axprecex  7821  negeq0  8152  muleqadd  8565  fihasheq0  10707  cjne0  10850  sqrt00  10982  sqrtmsq2i  11077  cbvsum  11301  fsump1i  11374  mertenslem2  11477  cbvprod  11499  absefib  11711  efieq1re  11712  lgsdinn0  13599  iswomninnlem  13938