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  3847  preqsn  3852  opeqpr  4339  orddif  4638  dfrel4v  5179  dfiota2  5278  funopg  5351  funopsn  5816  fnressn  5824  fressnfv  5825  riotaeqimp  5978  acexmidlemph  5993  fnovim  6112  tpossym  6420  qsid  6745  mapsncnv  6840  ixpsnf1o  6881  pw1fin  7068  ss1o0el1o  7071  unfiexmid  7076  onntri35  7418  recidpirq  8041  axprecex  8063  negeq0  8396  muleqadd  8811  fihasheq0  11010  cjne0  11414  sqrt00  11546  sqrtmsq2i  11641  cbvsum  11866  fsump1i  11939  mertenslem2  12042  cbvprod  12064  absefib  12277  efieq1re  12278  isnsg4  13744  plyco  15427  lgsdinn0  15721  m1lgs  15758  upgrex  15897  uhgr2edg  15998  usgredg2vlem1  16014  usgredg2vlem2  16015  ushgredgedg  16018  ushgredgedgloop  16020  iswomninnlem  16376