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  3310  dfss1  3341  disj  3473  disjr  3474  undisj1  3482  undisj2  3483  uneqdifeqim  3510  reusn  3665  rabsneu  3667  eusn  3668  iin0r  4171  opeqsn  4254  unisuc  4415  onsucelsucexmid  4531  sucprcreg  4550  onintexmid  4574  dmopab3  4842  dm0rn0  4846  ssdmres  4931  imadisj  4992  args  4999  intirr  5017  dminxp  5075  dfrel3  5088  fntpg  5274  fncnv  5284  f0rn0  5412  dff1o4  5471  dffv4g  5514  fvun2  5585  fnreseql  5628  riota1  5851  riota2df  5853  fnotovb  5920  ovid  5993  ov  5996  ovg  6015  f1od2  6238  frec0g  6400  diffitest  6889  ismkvnex  7155  prarloclem5  7501  renegcl  8220  elznn0  9270  hashunlem  10786  maxclpr  11233  lgseisenlem1  14489  ex-ceil  14517  nninfsellemqall  14803  nninfomni  14807  iswomni0  14838