Theorem eqeq1i 2214

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

Syntax hints:   ↔ wb 105   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  ssequn2  3350  dfss1  3381  disj  3513  disjr  3514  undisj1  3522  undisj2  3523  uneqdifeqim  3550  reusn  3709  rabsneu  3711  eusn  3712  iin0r  4221  opeqsn  4305  unisuc  4468  onsucelsucexmid  4586  sucprcreg  4605  onintexmid  4629  dmopab3  4900  dm0rn0  4904  ssdmres  4990  imadisj  5053  args  5060  intirr  5078  dminxp  5136  dfrel3  5149  fntpg  5339  fncnv  5349  f0rn0  5482  dff1o4  5542  dffv4g  5586  fvun2  5659  fnreseql  5703  funopdmsn  5777  riota1  5931  riota2df  5933  fnotovb  6001  ovid  6075  ov  6078  ovg  6098  f1od2  6334  frec0g  6496  diffitest  6999  ismkvnex  7272  prarloclem5  7633  renegcl  8353  elznn0  9407  seqf1oglem1  10686  seqf1oglem2  10687  hashunlem  10971  maxclpr  11608  gausslemma2d  15621  lgseisenlem1  15622  2lgslem4  15655  edg0iedg0g  15737  ex-ceil  15801  nninfsellemqall  16093  nninfomni  16097  iswomni0  16131