Theorem eqeq1i 2204

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

Syntax hints:   ↔ wb 105   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  ssequn2  3337  dfss1  3368  disj  3500  disjr  3501  undisj1  3509  undisj2  3510  uneqdifeqim  3537  reusn  3694  rabsneu  3696  eusn  3697  iin0r  4203  opeqsn  4286  unisuc  4449  onsucelsucexmid  4567  sucprcreg  4586  onintexmid  4610  dmopab3  4880  dm0rn0  4884  ssdmres  4969  imadisj  5032  args  5039  intirr  5057  dminxp  5115  dfrel3  5128  fntpg  5315  fncnv  5325  f0rn0  5455  dff1o4  5515  dffv4g  5558  fvun2  5631  fnreseql  5675  riota1  5899  riota2df  5901  fnotovb  5969  ovid  6043  ov  6046  ovg  6066  f1od2  6302  frec0g  6464  diffitest  6957  ismkvnex  7230  prarloclem5  7584  renegcl  8304  elznn0  9358  seqf1oglem1  10628  seqf1oglem2  10629  hashunlem  10913  maxclpr  11404  gausslemma2d  15394  lgseisenlem1  15395  2lgslem4  15428  ex-ceil  15456  nninfsellemqall  15746  nninfomni  15750  iswomni0  15782