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  5833  riota1  5990  riota2df  5992  riotaeqimp  5995  fnbrovb  6062  fnotovb  6063  ovid  6137  ov  6140  ovg  6160  f1od2  6399  frec0g  6562  diffitest  7075  ismkvnex  7353  prarloclem5  7719  renegcl  8439  elznn0  9493  seqf1oglem1  10780  seqf1oglem2  10781  hashunlem  11066  maxclpr  11782  gausslemma2d  15797  lgseisenlem1  15798  2lgslem4  15831  edg0iedg0g  15916  ushgredgedg  16076  ushgredgedgloop  16078  uhgr0v0e  16084  1loopgrvd2fi  16155  ex-ceil  16322  nninfsellemqall  16617  nninfomni  16621  iswomni0  16655