Theorem eqeq2i 2151

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

Syntax hints:   ↔ wb 104   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  eqtri  2161  rabid2  2610  dfss2  3091  equncom  3226  preq12b  3705  preqsn  3710  opeqpr  4183  orddif  4470  dfrel4v  4998  dfiota2  5097  funopg  5165  fnressn  5614  fressnfv  5615  acexmidlemph  5775  fnovim  5887  tpossym  6181  qsid  6502  mapsncnv  6597  ixpsnf1o  6638  unfiexmid  6814  recidpirq  7690  axprecex  7712  negeq0  8040  muleqadd  8453  fihasheq0  10572  cjne0  10712  sqrt00  10844  sqrtmsq2i  10939  cbvsum  11161  fsump1i  11234  mertenslem2  11337  cbvprod  11359  absefib  11513  efieq1re  11514  iswomninnlem  13417