Theorem eqeq2i 2240

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

Syntax hints:   ↔ wb 105   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtri  2250  rabid2  2708  ssalel  3212  equncom  3349  preq12b  3848  preqsn  3853  opeqpr  4340  orddif  4639  dfrel4v  5180  dfiota2  5279  funopg  5352  funopsn  5819  fnressn  5829  fressnfv  5830  riotaeqimp  5985  acexmidlemph  6000  fnovim  6119  tpossym  6428  qsid  6755  mapsncnv  6850  ixpsnf1o  6891  pw1fin  7083  ss1o0el1o  7086  unfiexmid  7091  onntri35  7433  recidpirq  8056  axprecex  8078  negeq0  8411  muleqadd  8826  fihasheq0  11027  cjne0  11434  sqrt00  11566  sqrtmsq2i  11661  cbvsum  11886  fsump1i  11959  mertenslem2  12062  cbvprod  12084  absefib  12297  efieq1re  12298  isnsg4  13764  plyco  15448  lgsdinn0  15742  m1lgs  15779  upgrex  15918  uhgr2edg  16019  usgredg2vlem1  16035  usgredg2vlem2  16036  ushgredgedg  16039  ushgredgedgloop  16041  iswomninnlem  16477