Theorem eqeq2i 2242

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

Syntax hints:   ↔ wb 105   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtri  2252  rabid2  2710  ssalel  3215  equncom  3352  preq12b  3853  preqsn  3858  opeqpr  4346  orddif  4645  dfrel4v  5188  dfiota2  5287  funopg  5360  funopsn  5830  fnressn  5840  fressnfv  5841  riotaeqimp  5996  acexmidlemph  6011  fnovim  6130  tpossym  6442  qsid  6769  mapsncnv  6864  ixpsnf1o  6905  pw1fin  7102  ss1o0el1o  7105  unfiexmid  7110  onntri35  7455  recidpirq  8078  axprecex  8100  negeq0  8433  muleqadd  8848  fihasheq0  11056  cjne0  11473  sqrt00  11605  sqrtmsq2i  11700  cbvsum  11925  fsump1i  11999  mertenslem2  12102  cbvprod  12124  absefib  12337  efieq1re  12338  isnsg4  13804  plyco  15489  lgsdinn0  15783  m1lgs  15820  upgrex  15960  uhgr2edg  16063  usgredg2vlem1  16079  usgredg2vlem2  16080  ushgredgedg  16083  ushgredgedgloop  16085  iswomninnlem  16680