Theorem eqeq2i 2181

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

Syntax hints:   ↔ wb 104   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  eqtri  2191  rabid2  2646  dfss2  3136  equncom  3272  preq12b  3757  preqsn  3762  opeqpr  4238  orddif  4531  dfrel4v  5062  dfiota2  5161  funopg  5232  fnressn  5682  fressnfv  5683  acexmidlemph  5846  fnovim  5961  tpossym  6255  qsid  6578  mapsncnv  6673  ixpsnf1o  6714  pw1fin  6888  ss1o0el1o  6890  unfiexmid  6895  onntri35  7214  recidpirq  7820  axprecex  7842  negeq0  8173  muleqadd  8586  fihasheq0  10728  cjne0  10872  sqrt00  11004  sqrtmsq2i  11099  cbvsum  11323  fsump1i  11396  mertenslem2  11499  cbvprod  11521  absefib  11733  efieq1re  11734  lgsdinn0  13743  iswomninnlem  14081