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  11161  sqrt00  11293  sqrtmsq2i  11388  cbvsum  11613  fsump1i  11686  mertenslem2  11789  cbvprod  11811  absefib  12024  efieq1re  12025  isnsg4  13490  plyco  15173  lgsdinn0  15467  m1lgs  15504  iswomninnlem  15921