Theorem eqeq2i 2217

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

Syntax hints:   ↔ wb 105   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtri  2227  rabid2  2684  ssalel  3185  equncom  3322  preq12b  3819  preqsn  3824  opeqpr  4311  orddif  4608  dfrel4v  5148  dfiota2  5247  funopg  5319  funopsn  5780  fnressn  5788  fressnfv  5789  acexmidlemph  5955  fnovim  6072  tpossym  6380  qsid  6705  mapsncnv  6800  ixpsnf1o  6841  pw1fin  7028  ss1o0el1o  7031  unfiexmid  7036  onntri35  7378  recidpirq  8001  axprecex  8023  negeq0  8356  muleqadd  8771  fihasheq0  10970  cjne0  11304  sqrt00  11436  sqrtmsq2i  11531  cbvsum  11756  fsump1i  11829  mertenslem2  11932  cbvprod  11954  absefib  12167  efieq1re  12168  isnsg4  13633  plyco  15316  lgsdinn0  15610  m1lgs  15647  upgrex  15784  iswomninnlem  16160