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  dfss2  3172  equncom  3308  preq12b  3800  preqsn  3805  opeqpr  4286  orddif  4583  dfrel4v  5121  dfiota2  5220  funopg  5292  fnressn  5748  fressnfv  5749  acexmidlemph  5915  fnovim  6031  tpossym  6334  qsid  6659  mapsncnv  6754  ixpsnf1o  6795  pw1fin  6971  ss1o0el1o  6974  unfiexmid  6979  onntri35  7304  recidpirq  7925  axprecex  7947  negeq0  8280  muleqadd  8695  fihasheq0  10885  cjne0  11073  sqrt00  11205  sqrtmsq2i  11300  cbvsum  11525  fsump1i  11598  mertenslem2  11701  cbvprod  11723  absefib  11936  efieq1re  11937  isnsg4  13342  plyco  14995  lgsdinn0  15289  m1lgs  15326  iswomninnlem  15693