Theorem eqeq2i 2243

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

Syntax hints:   ↔ wb 105   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqtri  2253  rabid2  2721  ssalel  3226  equncom  3364  preq12b  3874  preqsn  3879  opeqpr  4370  orddif  4669  dfrel4v  5214  dfiota2  5313  funopg  5386  funopsn  5860  fnressn  5870  fressnfv  5871  riotaeqimp  6028  acexmidlemph  6043  fnovim  6162  tpossym  6507  qsid  6834  mapsncnv  6930  ixpsnf1o  6971  pw1fin  7170  ss1o0el1o  7173  unfiexmid  7178  onntri35  7547  recidpirq  8173  axprecex  8195  negeq0  8527  muleqadd  8942  fihasheq0  11156  hashfibc  11207  cjne0  11593  sqrt00  11725  sqrtmsq2i  11820  cbvsum  12045  fsump1i  12119  mertenslem2  12222  cbvprod  12244  absefib  12457  efieq1re  12458  isnsg4  13929  plyco  15624  lgsdinn0  15921  m1lgs  15958  upgrex  16098  uhgr2edg  16201  usgredg2vlem1  16217  usgredg2vlem2  16218  ushgredgedg  16221  ushgredgedgloop  16223  exmidnotnotr  16779  iswomninnlem  16834