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  3145  equncom  3281  preq12b  3771  preqsn  3776  opeqpr  4254  orddif  4547  dfrel4v  5081  dfiota2  5180  funopg  5251  fnressn  5703  fressnfv  5704  acexmidlemph  5868  fnovim  5983  tpossym  6277  qsid  6600  mapsncnv  6695  ixpsnf1o  6736  pw1fin  6910  ss1o0el1o  6912  unfiexmid  6917  onntri35  7236  recidpirq  7857  axprecex  7879  negeq0  8211  muleqadd  8625  fihasheq0  10773  cjne0  10917  sqrt00  11049  sqrtmsq2i  11144  cbvsum  11368  fsump1i  11441  mertenslem2  11544  cbvprod  11566  absefib  11778  efieq1re  11779  isnsg4  13072  lgsdinn0  14452  m1lgs  14455  iswomninnlem  14800