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 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqabb  2374  ssequn2  3402  ineqcom  3422  dfss1  3435  disj  3572  disjr  3573  undisj1  3581  undisj2  3582  uneqdifeqim  3610  reusn  3778  rabsneu  3780  eusn  3781  iin0r  4301  opeqsn  4388  unisuc  4553  onsucelsucexmid  4672  sucprcreg  4691  onintexmid  4715  dmopab3  4989  dm0rn0  4993  ssdmres  5080  imadisj  5144  args  5151  intirr  5169  dminxp  5227  dfrel3  5240  cbviotavw  5338  fntpg  5432  fncnv  5442  fresaunres1disj  5566  f0rn0  5582  dff1o4  5642  dffv4g  5687  fvun2  5764  fnreseql  5810  funopdmsn  5886  riota1  6048  riota2df  6050  riotaeqimp  6053  fnbrovb  6120  fnotovb  6121  ovid  6195  ov  6198  ovg  6218  f1od2  6461  frec0g  6658  diffitest  7181  ismkvnex  7485  prarloclem5  7857  renegcl  8577  addeq0  8693  elznn0  9638  seqf1oglem1  10934  seqf1oglem2  10935  hashunlem  11222  maxclpr  11966  gausslemma2d  16102  lgseisenlem1  16103  2lgslem4  16136  edg0iedg0g  16221  ushgredgedg  16381  ushgredgedgloop  16383  uhgr0v0e  16389  1loopgrvd2fi  16460  ex-ceil  16654  nninfsellemqall  16963  nninfomni  16967  iswomni0  17006