Theorem eqeq1i 2178

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

Syntax hints:   ↔ wb 104   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  ssequn2  3300  dfss1  3331  disj  3463  disjr  3464  undisj1  3472  undisj2  3473  uneqdifeqim  3500  reusn  3654  rabsneu  3656  eusn  3657  iin0r  4155  opeqsn  4237  unisuc  4398  onsucelsucexmid  4514  sucprcreg  4533  onintexmid  4557  dmopab3  4824  dm0rn0  4828  ssdmres  4913  imadisj  4973  args  4980  intirr  4997  dminxp  5055  dfrel3  5068  fntpg  5254  fncnv  5264  f0rn0  5392  dff1o4  5450  dffv4g  5493  fvun2  5563  fnreseql  5606  riota1  5827  riota2df  5829  fnotovb  5896  ovid  5969  ov  5972  ovg  5991  f1od2  6214  frec0g  6376  diffitest  6865  ismkvnex  7131  prarloclem5  7462  renegcl  8180  elznn0  9227  hashunlem  10739  maxclpr  11186  ex-ceil  13761  nninfsellemqall  14048  nninfomni  14052  iswomni0  14083