Theorem eqeq2i 2242

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

Syntax hints:   ↔ wb 105   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  eqtri  2252  rabid2  2710  ssalel  3215  equncom  3352  preq12b  3853  preqsn  3858  opeqpr  4346  orddif  4645  dfrel4v  5188  dfiota2  5287  funopg  5360  funopsn  5829  fnressn  5839  fressnfv  5840  riotaeqimp  5995  acexmidlemph  6010  fnovim  6129  tpossym  6441  qsid  6768  mapsncnv  6863  ixpsnf1o  6904  pw1fin  7101  ss1o0el1o  7104  unfiexmid  7109  onntri35  7454  recidpirq  8077  axprecex  8099  negeq0  8432  muleqadd  8847  fihasheq0  11054  cjne0  11468  sqrt00  11600  sqrtmsq2i  11695  cbvsum  11920  fsump1i  11993  mertenslem2  12096  cbvprod  12118  absefib  12331  efieq1re  12332  isnsg4  13798  plyco  15482  lgsdinn0  15776  m1lgs  15813  upgrex  15953  uhgr2edg  16056  usgredg2vlem1  16072  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  iswomninnlem  16653