Theorem eqeq1i 2239

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

Syntax hints:   ↔ wb 105   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  ssequn2  3382  dfss1  3413  disj  3545  disjr  3546  undisj1  3554  undisj2  3555  uneqdifeqim  3582  reusn  3746  rabsneu  3748  eusn  3749  iin0r  4265  opeqsn  4351  unisuc  4516  onsucelsucexmid  4634  sucprcreg  4653  onintexmid  4677  dmopab3  4950  dm0rn0  4954  ssdmres  5041  imadisj  5105  args  5112  intirr  5130  dminxp  5188  dfrel3  5201  cbviotavw  5299  fntpg  5393  fncnv  5403  f0rn0  5540  dff1o4  5600  dffv4g  5645  fvun2  5722  fnreseql  5766  funopdmsn  5842  riota1  6001  riota2df  6003  riotaeqimp  6006  fnbrovb  6073  fnotovb  6074  ovid  6148  ov  6151  ovg  6171  f1od2  6409  frec0g  6606  diffitest  7119  ismkvnex  7397  prarloclem5  7763  renegcl  8482  elznn0  9538  seqf1oglem1  10827  seqf1oglem2  10828  hashunlem  11113  maxclpr  11845  gausslemma2d  15871  lgseisenlem1  15872  2lgslem4  15905  edg0iedg0g  15990  ushgredgedg  16150  ushgredgedgloop  16152  uhgr0v0e  16158  1loopgrvd2fi  16229  ex-ceil  16423  nninfsellemqall  16724  nninfomni  16728  iswomni0  16767