Theorem eqeq2i 2240

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

Syntax hints:   ↔ wb 105   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtri  2250  rabid2  2708  ssalel  3213  equncom  3350  preq12b  3851  preqsn  3856  opeqpr  4344  orddif  4643  dfrel4v  5186  dfiota2  5285  funopg  5358  funopsn  5825  fnressn  5835  fressnfv  5836  riotaeqimp  5991  acexmidlemph  6006  fnovim  6125  tpossym  6437  qsid  6764  mapsncnv  6859  ixpsnf1o  6900  pw1fin  7095  ss1o0el1o  7098  unfiexmid  7103  onntri35  7445  recidpirq  8068  axprecex  8090  negeq0  8423  muleqadd  8838  fihasheq0  11045  cjne0  11459  sqrt00  11591  sqrtmsq2i  11686  cbvsum  11911  fsump1i  11984  mertenslem2  12087  cbvprod  12109  absefib  12322  efieq1re  12323  isnsg4  13789  plyco  15473  lgsdinn0  15767  m1lgs  15804  upgrex  15944  uhgr2edg  16045  usgredg2vlem1  16061  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  iswomninnlem  16589