Theorem eqeq1i 2029

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	⊢ A = B

Assertion

Ref	Expression
eqeq1i	⊢ (A = 𝐶 ↔ B = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ A = B
2		eqeq1 2028	. 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))
3	1, 2	ax-mp 7	1 ⊢ (A = 𝐶 ↔ B = 𝐶)

Syntax hints:   ↔ wb 98   = wceq 1228

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-cleq 2015

This theorem is referenced by:  ssequn2  3093  dfss1  3118  disj  3245  disjr  3246  undisj1  3256  undisj2  3257  uneqdifeqim  3285  reusn  3415  rabsneu  3417  eusn  3418  iin0r  3896  opeqsn  3963  unisuc  4099  onsucelsucexmid  4199  sucprcreg  4211  dmopab3  4475  dm0rn0  4479  ssdmres  4560  imadisj  4614  args  4621  intirr  4638  dminxp  4692  dfrel3  4705  fntpg  4881  fncnv  4891  dff1o4  5059  dffv4g  5100  fvun2  5165  fnreseql  5202  riota1  5410  riota2df  5412  fnotovb  5471  ovid  5540  ov  5543  ovg  5562  prarloclem5  6354  renegcl  6858