Theorem eqeq1i 2044

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 2043	. 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))
3	1, 2	ax-mp 7	1 ⊢ (A = 𝐶 ↔ B = 𝐶)

Syntax hints:   ↔ wb 98   = wceq 1242

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  ssequn2  3110  dfss1  3135  disj  3262  disjr  3263  undisj1  3273  undisj2  3274  uneqdifeqim  3302  reusn  3432  rabsneu  3434  eusn  3435  iin0r  3913  opeqsn  3980  unisuc  4116  onsucelsucexmid  4215  sucprcreg  4227  dmopab3  4491  dm0rn0  4495  ssdmres  4576  imadisj  4630  args  4637  intirr  4654  dminxp  4708  dfrel3  4721  fntpg  4898  fncnv  4908  dff1o4  5077  dffv4g  5118  fvun2  5183  fnreseql  5220  riota1  5429  riota2df  5431  fnotovb  5490  ovid  5559  ov  5562  ovg  5581  frec0g  5922  prarloclem5  6482  renegcl  7028  elznn0  7996