Theorem eqeq1i 2201

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 2200	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  ssequn2  3332  dfss1  3363  disj  3495  disjr  3496  undisj1  3504  undisj2  3505  uneqdifeqim  3532  reusn  3689  rabsneu  3691  eusn  3692  iin0r  4198  opeqsn  4281  unisuc  4444  onsucelsucexmid  4562  sucprcreg  4581  onintexmid  4605  dmopab3  4875  dm0rn0  4879  ssdmres  4964  imadisj  5027  args  5034  intirr  5052  dminxp  5110  dfrel3  5123  fntpg  5310  fncnv  5320  f0rn0  5448  dff1o4  5508  dffv4g  5551  fvun2  5624  fnreseql  5668  riota1  5892  riota2df  5894  fnotovb  5961  ovid  6035  ov  6038  ovg  6057  f1od2  6288  frec0g  6450  diffitest  6943  ismkvnex  7214  prarloclem5  7560  renegcl  8280  elznn0  9332  seqf1oglem1  10590  seqf1oglem2  10591  hashunlem  10875  maxclpr  11366  gausslemma2d  15185  lgseisenlem1  15186  ex-ceil  15218  nninfsellemqall  15505  nninfomni  15509  iswomni0  15541