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 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtri  2259  eqabbw  2375  rabid2  2729  ssalel  3235  equncom  3374  ab0w  3550  preq12b  3895  preqsn  3900  opeqpr  4396  orddif  4696  dfrel4v  5242  dfiota2  5341  funopg  5414  funopsn  5894  fnressn  5904  fressnfv  5905  riotaeqimp  6066  acexmidlemph  6081  fnovim  6200  tpossym  6551  qsid  6878  mapsncnv  6981  ixpsnf1o  7022  pw1fin  7221  ss1o0el1o  7224  unfiexmid  7229  onntri35  7602  recidpirq  8231  axprecex  8253  negeq0  8587  muleqadd  9006  fihasheq0  11254  hashfibc  11305  hashf1lem2  11308  cjne0  11696  sqrt00  11828  sqrtmsq2i  11924  cbvsum  12151  fsump1i  12225  mertenslem2  12328  cbvprod  12350  absefib  12563  efieq1re  12564  isnsg4  14074  isassa  15111  plyco  15985  sineq0re  16076  ppiqub  16293  lgsdinn0  16372  m1lgs  16409  upgrex  16549  uhgr2edg  16652  usgredg2vlem1  16668  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  exmidnotnotr  17241  iswomninnlem  17306