Theorem eqeq1i 2185

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

Syntax hints:   ↔ wb 105   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  ssequn2  3308  dfss1  3339  disj  3471  disjr  3472  undisj1  3480  undisj2  3481  uneqdifeqim  3508  reusn  3663  rabsneu  3665  eusn  3666  iin0r  4169  opeqsn  4252  unisuc  4413  onsucelsucexmid  4529  sucprcreg  4548  onintexmid  4572  dmopab3  4840  dm0rn0  4844  ssdmres  4929  imadisj  4990  args  4997  intirr  5015  dminxp  5073  dfrel3  5086  fntpg  5272  fncnv  5282  f0rn0  5410  dff1o4  5469  dffv4g  5512  fvun2  5583  fnreseql  5626  riota1  5848  riota2df  5850  fnotovb  5917  ovid  5990  ov  5993  ovg  6012  f1od2  6235  frec0g  6397  diffitest  6886  ismkvnex  7152  prarloclem5  7498  renegcl  8217  elznn0  9267  hashunlem  10783  maxclpr  11230  lgseisenlem1  14386  ex-ceil  14414  nninfsellemqall  14700  nninfomni  14704  iswomni0  14735