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 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 2213

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

This theorem is referenced by:  eqtri  2252  rabid2  2711  ssalel  3216  equncom  3354  preq12b  3858  preqsn  3863  opeqpr  4352  orddif  4651  dfrel4v  5195  dfiota2  5294  funopg  5367  funopsn  5838  fnressn  5848  fressnfv  5849  riotaeqimp  6006  acexmidlemph  6021  fnovim  6140  tpossym  6485  qsid  6812  mapsncnv  6907  ixpsnf1o  6948  pw1fin  7145  ss1o0el1o  7148  unfiexmid  7153  onntri35  7498  recidpirq  8121  axprecex  8143  negeq0  8475  muleqadd  8890  fihasheq0  11101  cjne0  11531  sqrt00  11663  sqrtmsq2i  11758  cbvsum  11983  fsump1i  12057  mertenslem2  12160  cbvprod  12182  absefib  12395  efieq1re  12396  isnsg4  13862  plyco  15553  lgsdinn0  15850  m1lgs  15887  upgrex  16027  uhgr2edg  16130  usgredg2vlem1  16146  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  exmidnotnotr  16710  iswomninnlem  16765