Theorem eqeq1i 2246

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 2245	. 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:  eqabb  2374  ssequn2  3402  ineqcom  3422  dfss1  3435  disj  3573  disjr  3574  undisj1  3582  undisj2  3583  uneqdifeqim  3613  reusn  3782  rabsneu  3784  eusn  3785  iin0r  4306  opeqsn  4393  unisuc  4558  onsucelsucexmid  4677  sucprcreg  4696  onintexmid  4720  dmopab3  4994  dm0rn0  4998  ssdmres  5085  imadisj  5149  args  5156  intirr  5174  dminxp  5232  dfrel3  5245  cbviotavw  5343  fntpg  5437  fncnv  5447  fresaunres1disj  5571  f0rn0  5587  dff1o4  5647  dffv4g  5692  fvun2  5770  fnreseql  5819  funopdmsn  5895  riota1  6058  riota2df  6060  riotaeqimp  6063  fnbrovb  6130  fnotovb  6131  ovid  6205  ov  6208  ovg  6228  f1od2  6471  frec0g  6668  diffitest  7191  ismkvnex  7495  prarloclem5  7867  renegcl  8587  addeq0  8703  elznn0  9659  seqf1oglem1  10956  seqf1oglem2  10957  hashunlem  11244  maxclpr  11988  gausslemma2d  16188  lgseisenlem1  16189  2lgslem4  16222  edg0iedg0g  16307  ushgredgedg  16467  ushgredgedgloop  16469  uhgr0v0e  16475  1loopgrvd2fi  16546  ex-ceil  16740  nninfsellemqall  17058  nninfomni  17062  iswomni0  17101