Theorem eqeq2i 2204

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

Syntax hints:   ↔ wb 105   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtri  2214  rabid2  2671  dfss2  3168  equncom  3304  preq12b  3796  preqsn  3801  opeqpr  4282  orddif  4579  dfrel4v  5117  dfiota2  5216  funopg  5288  fnressn  5744  fressnfv  5745  acexmidlemph  5911  fnovim  6027  tpossym  6329  qsid  6654  mapsncnv  6749  ixpsnf1o  6790  pw1fin  6966  ss1o0el1o  6969  unfiexmid  6974  onntri35  7297  recidpirq  7918  axprecex  7940  negeq0  8273  muleqadd  8687  fihasheq0  10864  cjne0  11052  sqrt00  11184  sqrtmsq2i  11279  cbvsum  11503  fsump1i  11576  mertenslem2  11679  cbvprod  11701  absefib  11914  efieq1re  11915  isnsg4  13282  lgsdinn0  15164  m1lgs  15192  iswomninnlem  15539