Theorem eqeq2i 2181

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

Syntax hints:   ↔ wb 104   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtri  2191  rabid2  2646  dfss2  3136  equncom  3272  preq12b  3755  preqsn  3760  opeqpr  4236  orddif  4529  dfrel4v  5060  dfiota2  5159  funopg  5230  fnressn  5679  fressnfv  5680  acexmidlemph  5843  fnovim  5958  tpossym  6252  qsid  6574  mapsncnv  6669  ixpsnf1o  6710  pw1fin  6884  ss1o0el1o  6886  unfiexmid  6891  onntri35  7201  recidpirq  7807  axprecex  7829  negeq0  8160  muleqadd  8573  fihasheq0  10715  cjne0  10859  sqrt00  10991  sqrtmsq2i  11086  cbvsum  11310  fsump1i  11383  mertenslem2  11486  cbvprod  11508  absefib  11720  efieq1re  11721  lgsdinn0  13664  iswomninnlem  14003