Theorem eqeq2i 2215

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

Syntax hints:   ↔ wb 105   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  eqtri  2225  rabid2  2682  ssalel  3180  equncom  3317  preq12b  3810  preqsn  3815  opeqpr  4297  orddif  4594  dfrel4v  5133  dfiota2  5232  funopg  5304  funopsn  5761  fnressn  5769  fressnfv  5770  acexmidlemph  5936  fnovim  6053  tpossym  6361  qsid  6686  mapsncnv  6781  ixpsnf1o  6822  pw1fin  7006  ss1o0el1o  7009  unfiexmid  7014  onntri35  7348  recidpirq  7970  axprecex  7992  negeq0  8325  muleqadd  8740  fihasheq0  10936  cjne0  11190  sqrt00  11322  sqrtmsq2i  11417  cbvsum  11642  fsump1i  11715  mertenslem2  11818  cbvprod  11840  absefib  12053  efieq1re  12054  isnsg4  13519  plyco  15202  lgsdinn0  15496  m1lgs  15533  iswomninnlem  15950