Theorem eqeq1i 2237

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 2236	. 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:  ssequn2  3377  dfss1  3408  disj  3540  disjr  3541  undisj1  3549  undisj2  3550  uneqdifeqim  3577  reusn  3737  rabsneu  3739  eusn  3740  iin0r  4253  opeqsn  4339  unisuc  4504  onsucelsucexmid  4622  sucprcreg  4641  onintexmid  4665  dmopab3  4936  dm0rn0  4940  ssdmres  5027  imadisj  5090  args  5097  intirr  5115  dminxp  5173  dfrel3  5186  cbviotavw  5284  fntpg  5377  fncnv  5387  f0rn0  5522  dff1o4  5582  dffv4g  5626  fvun2  5703  fnreseql  5747  funopdmsn  5823  riota1  5980  riota2df  5982  riotaeqimp  5985  fnbrovb  6052  fnotovb  6053  ovid  6127  ov  6130  ovg  6150  f1od2  6387  frec0g  6549  diffitest  7057  ismkvnex  7333  prarloclem5  7698  renegcl  8418  elznn0  9472  seqf1oglem1  10753  seqf1oglem2  10754  hashunlem  11038  maxclpr  11748  gausslemma2d  15763  lgseisenlem1  15764  2lgslem4  15797  edg0iedg0g  15881  ushgredgedg  16039  ushgredgedgloop  16041  ex-ceil  16145  nninfsellemqall  16441  nninfomni  16445  iswomni0  16479