Theorem eqeq1i 2162

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

Syntax hints:   ↔ wb 104   = wceq 1332

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 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136

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

This theorem is referenced by:  ssequn2  3276  dfss1  3307  disj  3438  disjr  3439  undisj1  3447  undisj2  3448  uneqdifeqim  3475  reusn  3626  rabsneu  3628  eusn  3629  iin0r  4125  opeqsn  4207  unisuc  4368  onsucelsucexmid  4483  sucprcreg  4502  onintexmid  4526  dmopab3  4792  dm0rn0  4796  ssdmres  4881  imadisj  4941  args  4948  intirr  4965  dminxp  5023  dfrel3  5036  fntpg  5219  fncnv  5229  f0rn0  5357  dff1o4  5415  dffv4g  5458  fvun2  5528  fnreseql  5570  riota1  5788  riota2df  5790  fnotovb  5854  ovid  5927  ov  5930  ovg  5949  f1od2  6172  frec0g  6334  diffitest  6821  ismkvnex  7077  prarloclem5  7399  renegcl  8115  elznn0  9161  hashunlem  10655  maxclpr  11099  ex-ceil  13248  nninfsellemqall  13536  nninfomni  13540  iswomni0  13571