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  7496  prarloclem5  7868  renegcl  8589  addeq0  8705  elznn0  9664  seqf1oglem1  10971  seqf1oglem2  10972  hashunlem  11260  maxclpr  12005  gausslemma2d  16354  lgseisenlem1  16355  2lgslem4  16388  edg0iedg0g  16473  ushgredgedg  16633  ushgredgedgloop  16635  uhgr0v0e  16641  1loopgrvd2fi  16712  ex-ceil  16906  nninfsellemqall  17224  nninfomni  17228  iswomni0  17268