Theorem eqeq1i 2204

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

Syntax hints:   ↔ wb 105   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  ssequn2  3336  dfss1  3367  disj  3499  disjr  3500  undisj1  3508  undisj2  3509  uneqdifeqim  3536  reusn  3693  rabsneu  3695  eusn  3696  iin0r  4202  opeqsn  4285  unisuc  4448  onsucelsucexmid  4566  sucprcreg  4585  onintexmid  4609  dmopab3  4879  dm0rn0  4883  ssdmres  4968  imadisj  5031  args  5038  intirr  5056  dminxp  5114  dfrel3  5127  fntpg  5314  fncnv  5324  f0rn0  5452  dff1o4  5512  dffv4g  5555  fvun2  5628  fnreseql  5672  riota1  5896  riota2df  5898  fnotovb  5965  ovid  6039  ov  6042  ovg  6062  f1od2  6293  frec0g  6455  diffitest  6948  ismkvnex  7221  prarloclem5  7567  renegcl  8287  elznn0  9341  seqf1oglem1  10611  seqf1oglem2  10612  hashunlem  10896  maxclpr  11387  gausslemma2d  15310  lgseisenlem1  15311  2lgslem4  15344  ex-ceil  15372  nninfsellemqall  15659  nninfomni  15663  iswomni0  15695