Theorem eqeq1i 2173

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

Syntax hints:   ↔ wb 104   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  ssequn2  3295  dfss1  3326  disj  3457  disjr  3458  undisj1  3466  undisj2  3467  uneqdifeqim  3494  reusn  3647  rabsneu  3649  eusn  3650  iin0r  4148  opeqsn  4230  unisuc  4391  onsucelsucexmid  4507  sucprcreg  4526  onintexmid  4550  dmopab3  4817  dm0rn0  4821  ssdmres  4906  imadisj  4966  args  4973  intirr  4990  dminxp  5048  dfrel3  5061  fntpg  5244  fncnv  5254  f0rn0  5382  dff1o4  5440  dffv4g  5483  fvun2  5553  fnreseql  5595  riota1  5816  riota2df  5818  fnotovb  5885  ovid  5958  ov  5961  ovg  5980  f1od2  6203  frec0g  6365  diffitest  6853  ismkvnex  7119  prarloclem5  7441  renegcl  8159  elznn0  9206  hashunlem  10717  maxclpr  11164  ex-ceil  13607  nninfsellemqall  13895  nninfomni  13899  iswomni0  13930