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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  ssequn2  3380  dfss1  3411  disj  3543  disjr  3544  undisj1  3552  undisj2  3553  uneqdifeqim  3580  reusn  3742  rabsneu  3744  eusn  3745  iin0r  4259  opeqsn  4345  unisuc  4510  onsucelsucexmid  4628  sucprcreg  4647  onintexmid  4671  dmopab3  4944  dm0rn0  4948  ssdmres  5035  imadisj  5098  args  5105  intirr  5123  dminxp  5181  dfrel3  5194  cbviotavw  5292  fntpg  5386  fncnv  5396  f0rn0  5531  dff1o4  5591  dffv4g  5636  fvun2  5713  fnreseql  5757  funopdmsn  5834  riota1  5991  riota2df  5993  riotaeqimp  5996  fnbrovb  6063  fnotovb  6064  ovid  6138  ov  6141  ovg  6161  f1od2  6400  frec0g  6563  diffitest  7076  ismkvnex  7354  prarloclem5  7720  renegcl  8440  elznn0  9494  seqf1oglem1  10782  seqf1oglem2  10783  hashunlem  11068  maxclpr  11787  gausslemma2d  15804  lgseisenlem1  15805  2lgslem4  15838  edg0iedg0g  15923  ushgredgedg  16083  ushgredgedgloop  16085  uhgr0v0e  16091  1loopgrvd2fi  16162  ex-ceil  16344  nninfsellemqall  16643  nninfomni  16647  iswomni0  16682