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  2653  dfss2  3144  equncom  3280  preq12b  3769  preqsn  3774  opeqpr  4251  orddif  4544  dfrel4v  5077  dfiota2  5176  funopg  5247  fnressn  5699  fressnfv  5700  acexmidlemph  5863  fnovim  5978  tpossym  6272  qsid  6595  mapsncnv  6690  ixpsnf1o  6731  pw1fin  6905  ss1o0el1o  6907  unfiexmid  6912  onntri35  7231  recidpirq  7852  axprecex  7874  negeq0  8205  muleqadd  8619  fihasheq0  10764  cjne0  10908  sqrt00  11040  sqrtmsq2i  11135  cbvsum  11359  fsump1i  11432  mertenslem2  11535  cbvprod  11557  absefib  11769  efieq1re  11770  lgsdinn0  14231  iswomninnlem  14568