Theorem eqeq1i 2047

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

Syntax hints:   ↔ wb 98   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  ssequn2  3116  dfss1  3141  disj  3268  disjr  3269  undisj1  3279  undisj2  3280  uneqdifeqim  3308  reusn  3441  rabsneu  3443  eusn  3444  iin0r  3922  opeqsn  3989  unisuc  4150  onsucelsucexmid  4255  sucprcreg  4273  onintexmid  4297  dmopab3  4548  dm0rn0  4552  ssdmres  4633  imadisj  4687  args  4694  intirr  4711  dminxp  4765  dfrel3  4778  fntpg  4955  fncnv  4965  dff1o4  5134  dffv4g  5175  fvun2  5240  fnreseql  5277  riota1  5486  riota2df  5488  fnotovb  5548  ovid  5617  ov  5620  ovg  5639  frec0g  5983  diffitest  6344  prarloclem5  6598  renegcl  7272  elznn0  8260  ex-ceil  9896