Theorem eqeq1i 2242

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 2241	. 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 2216

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

This theorem is referenced by:  eqabb  2370  ssequn2  3396  ineqcom  3416  dfss1  3429  disj  3562  disjr  3563  undisj1  3571  undisj2  3572  uneqdifeqim  3600  reusn  3768  rabsneu  3770  eusn  3771  iin0r  4288  opeqsn  4375  unisuc  4540  onsucelsucexmid  4659  sucprcreg  4678  onintexmid  4702  dmopab3  4976  dm0rn0  4980  ssdmres  5067  imadisj  5131  args  5138  intirr  5156  dminxp  5214  dfrel3  5227  cbviotavw  5325  fntpg  5419  fncnv  5429  fresaunres1disj  5553  f0rn0  5569  dff1o4  5629  dffv4g  5674  fvun2  5751  fnreseql  5795  funopdmsn  5871  riota1  6033  riota2df  6035  riotaeqimp  6038  fnbrovb  6105  fnotovb  6106  ovid  6180  ov  6183  ovg  6203  f1od2  6446  frec0g  6643  diffitest  7159  ismkvnex  7461  prarloclem5  7833  renegcl  8553  addeq0  8669  elznn0  9614  seqf1oglem1  10910  seqf1oglem2  10911  hashunlem  11198  maxclpr  11938  gausslemma2d  16074  lgseisenlem1  16075  2lgslem4  16108  edg0iedg0g  16193  ushgredgedg  16353  ushgredgedgloop  16355  uhgr0v0e  16361  1loopgrvd2fi  16432  ex-ceil  16626  nninfsellemqall  16935  nninfomni  16939  iswomni0  16978