Theorem eqeq2i 2091

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

Syntax hints:   ↔ wb 103   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqtri  2101  rabid2  2530  dfss2  2988  equncom  3117  preq12b  3562  preqsn  3567  opeqpr  4008  orddif  4290  dfrel4v  4792  dfiota2  4888  funopg  4954  fnressn  5370  fressnfv  5371  acexmidlemph  5525  fnovim  5629  tpossym  5914  tfr0  5960  qsid  6194  recidpirq  7026  axprecex  7046  negeq0  7362  muleqadd  7758  cjne0  9795  sqrt00  9926  sqrtmsq2i  10021