Theorem eqeq2i 2249

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

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtri  2259  eqabbw  2375  rabid2  2729  ssalel  3235  equncom  3374  ab0w  3550  preq12b  3895  preqsn  3900  opeqpr  4394  orddif  4694  dfrel4v  5239  dfiota2  5338  funopg  5411  funopsn  5891  fnressn  5901  fressnfv  5902  riotaeqimp  6063  acexmidlemph  6078  fnovim  6197  tpossym  6547  qsid  6874  mapsncnv  6977  ixpsnf1o  7018  pw1fin  7217  ss1o0el1o  7220  unfiexmid  7225  onntri35  7597  recidpirq  8226  axprecex  8248  negeq0  8582  muleqadd  9001  fihasheq0  11248  hashfibc  11299  hashf1lem2  11302  cjne0  11690  sqrt00  11822  sqrtmsq2i  11918  cbvsum  12145  fsump1i  12219  mertenslem2  12322  cbvprod  12344  absefib  12557  efieq1re  12558  isnsg4  14068  isassa  15086  plyco  15951  ppiqub  16254  lgsdinn0  16333  m1lgs  16370  upgrex  16510  uhgr2edg  16613  usgredg2vlem1  16629  usgredg2vlem2  16630  ushgredgedg  16633  ushgredgedgloop  16635  exmidnotnotr  17202  iswomninnlem  17266