Theorem eqeq1i 2120

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

Syntax hints:   ↔ wb 104   = wceq 1312

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106

This theorem is referenced by:  ssequn2  3213  dfss1  3244  disj  3375  disjr  3376  undisj1  3384  undisj2  3385  uneqdifeqim  3412  reusn  3558  rabsneu  3560  eusn  3561  iin0r  4051  opeqsn  4132  unisuc  4293  onsucelsucexmid  4403  sucprcreg  4422  onintexmid  4445  dmopab3  4710  dm0rn0  4714  ssdmres  4797  imadisj  4857  args  4864  intirr  4881  dminxp  4939  dfrel3  4952  fntpg  5135  fncnv  5145  f0rn0  5273  dff1o4  5329  dffv4g  5370  fvun2  5440  fnreseql  5482  riota1  5700  riota2df  5702  fnotovb  5766  ovid  5839  ov  5842  ovg  5861  f1od2  6083  frec0g  6245  diffitest  6731  prarloclem5  7249  renegcl  7939  elznn0  8966  hashunlem  10436  maxclpr  10879  ex-ceil  12618  nninfsellemqall  12888  nninfomni  12892