Theorem eqeq1i 2212

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

Syntax hints:   ↔ wb 105   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  ssequn2  3345  dfss1  3376  disj  3508  disjr  3509  undisj1  3517  undisj2  3518  uneqdifeqim  3545  reusn  3703  rabsneu  3705  eusn  3706  iin0r  4212  opeqsn  4295  unisuc  4458  onsucelsucexmid  4576  sucprcreg  4595  onintexmid  4619  dmopab3  4889  dm0rn0  4893  ssdmres  4978  imadisj  5041  args  5048  intirr  5066  dminxp  5124  dfrel3  5137  fntpg  5324  fncnv  5334  f0rn0  5464  dff1o4  5524  dffv4g  5567  fvun2  5640  fnreseql  5684  riota1  5908  riota2df  5910  fnotovb  5978  ovid  6052  ov  6055  ovg  6075  f1od2  6311  frec0g  6473  diffitest  6966  ismkvnex  7239  prarloclem5  7595  renegcl  8315  elznn0  9369  seqf1oglem1  10645  seqf1oglem2  10646  hashunlem  10930  maxclpr  11452  gausslemma2d  15464  lgseisenlem1  15465  2lgslem4  15498  ex-ceil  15526  nninfsellemqall  15816  nninfomni  15820  iswomni0  15854