Theorem eqeq2i 2188

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

Syntax hints:   ↔ wb 105   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtri  2198  rabid2  2654  dfss2  3146  equncom  3282  preq12b  3772  preqsn  3777  opeqpr  4255  orddif  4548  dfrel4v  5082  dfiota2  5181  funopg  5252  fnressn  5704  fressnfv  5705  acexmidlemph  5870  fnovim  5985  tpossym  6279  qsid  6602  mapsncnv  6697  ixpsnf1o  6738  pw1fin  6912  ss1o0el1o  6914  unfiexmid  6919  onntri35  7238  recidpirq  7859  axprecex  7881  negeq0  8213  muleqadd  8627  fihasheq0  10775  cjne0  10919  sqrt00  11051  sqrtmsq2i  11146  cbvsum  11370  fsump1i  11443  mertenslem2  11546  cbvprod  11568  absefib  11780  efieq1re  11781  isnsg4  13077  lgsdinn0  14534  m1lgs  14537  iswomninnlem  14882