Theorem eqeq1i 2212

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq1i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq1 2211	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  ssequn2  3345  dfss1  3376  disj  3508  disjr  3509  undisj1  3517  undisj2  3518  uneqdifeqim  3545  reusn  3703  rabsneu  3705  eusn  3706  iin0r  4212  opeqsn  4296  unisuc  4459  onsucelsucexmid  4577  sucprcreg  4596  onintexmid  4620  dmopab3  4890  dm0rn0  4894  ssdmres  4980  imadisj  5043  args  5050  intirr  5068  dminxp  5126  dfrel3  5139  fntpg  5329  fncnv  5339  f0rn0  5469  dff1o4  5529  dffv4g  5572  fvun2  5645  fnreseql  5689  funopdmsn  5763  riota1  5917  riota2df  5919  fnotovb  5987  ovid  6061  ov  6064  ovg  6084  f1od2  6320  frec0g  6482  diffitest  6983  ismkvnex  7256  prarloclem5  7612  renegcl  8332  elznn0  9386  seqf1oglem1  10662  seqf1oglem2  10663  hashunlem  10947  maxclpr  11475  gausslemma2d  15488  lgseisenlem1  15489  2lgslem4  15522  ex-ceil  15595  nninfsellemqall  15885  nninfomni  15889  iswomni0  15923