Theorem eqeq2i 2245

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

Syntax hints:   ↔ wb 105   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqtri  2255  rabid2  2723  ssalel  3229  equncom  3368  preq12b  3879  preqsn  3884  opeqpr  4375  orddif  4674  dfrel4v  5219  dfiota2  5318  funopg  5391  funopsn  5865  fnressn  5875  fressnfv  5876  riotaeqimp  6036  acexmidlemph  6051  fnovim  6170  tpossym  6520  qsid  6847  mapsncnv  6943  ixpsnf1o  6984  pw1fin  7183  ss1o0el1o  7186  unfiexmid  7191  onntri35  7560  recidpirq  8189  axprecex  8211  negeq0  8543  muleqadd  8959  fihasheq0  11181  hashfibc  11232  cjne0  11618  sqrt00  11750  sqrtmsq2i  11845  cbvsum  12070  fsump1i  12144  mertenslem2  12247  cbvprod  12269  absefib  12482  efieq1re  12483  isnsg4  13965  plyco  15750  lgsdinn0  16047  m1lgs  16084  upgrex  16224  uhgr2edg  16327  usgredg2vlem1  16343  usgredg2vlem2  16344  ushgredgedg  16347  ushgredgedgloop  16349  exmidnotnotr  16905  iswomninnlem  16960