Theorem eqeq2i 2249

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

Syntax hints:   ↔ wb 105   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqtri  2259  eqabbw  2375  rabid2  2729  ssalel  3235  equncom  3374  ab0w  3550  preq12b  3890  preqsn  3895  opeqpr  4389  orddif  4689  dfrel4v  5234  dfiota2  5333  funopg  5406  funopsn  5882  fnressn  5892  fressnfv  5893  riotaeqimp  6053  acexmidlemph  6068  fnovim  6187  tpossym  6537  qsid  6864  mapsncnv  6967  ixpsnf1o  7008  pw1fin  7207  ss1o0el1o  7210  unfiexmid  7215  onntri35  7586  recidpirq  8215  axprecex  8237  negeq0  8570  muleqadd  8988  fihasheq0  11210  hashfibc  11261  hashf1lem2  11264  cjne0  11652  sqrt00  11784  sqrtmsq2i  11879  cbvsum  12104  fsump1i  12178  mertenslem2  12281  cbvprod  12303  absefib  12516  efieq1re  12517  isnsg4  13992  plyco  15783  lgsdinn0  16081  m1lgs  16118  upgrex  16258  uhgr2edg  16361  usgredg2vlem1  16377  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  exmidnotnotr  16949  iswomninnlem  17004