Theorem eqeq1i 2197

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 2196	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  ssequn2  3323  dfss1  3354  disj  3486  disjr  3487  undisj1  3495  undisj2  3496  uneqdifeqim  3523  reusn  3678  rabsneu  3680  eusn  3681  iin0r  4187  opeqsn  4270  unisuc  4431  onsucelsucexmid  4547  sucprcreg  4566  onintexmid  4590  dmopab3  4858  dm0rn0  4862  ssdmres  4947  imadisj  5008  args  5015  intirr  5033  dminxp  5091  dfrel3  5104  fntpg  5291  fncnv  5301  f0rn0  5429  dff1o4  5488  dffv4g  5531  fvun2  5604  fnreseql  5647  riota1  5871  riota2df  5873  fnotovb  5940  ovid  6014  ov  6017  ovg  6036  f1od2  6261  frec0g  6423  diffitest  6916  ismkvnex  7184  prarloclem5  7530  renegcl  8249  elznn0  9299  hashunlem  10819  maxclpr  11266  lgseisenlem1  14928  ex-ceil  14956  nninfsellemqall  15243  nninfomni  15247  iswomni0  15278