Theorem eqeq1i 2360

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 = C ↔ B = C)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ A = B
2		eqeq1 2359	. 2 ⊢ (A = B → (A = C ↔ B = C))
3	1, 2	ax-mp 5	1 ⊢ (A = C ↔ B = C)

Syntax hints:   ↔ wb 176   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  ssequn2  3436  dfss1  3460  dfss4  3489  disjr  3592  undisj1  3602  undisj2  3603  undif  3630  uneqdifeq  3638  reusn  3793  rabsneu  3795  eusn  3796  uniintsn  3963  dfiota4  4372  dfaddc2  4381  addccom  4406  addcass  4415  nndisjeq  4429  vfin1cltv  4547  phidisjnn  4615  opeqexb  4620  dmopab3  4917  dm0rn0  4921  ssdmres  4987  resabs1  4992  imadisj  5015  intirr  5029  dminxp  5061  funun  5146  fncnv  5158  dff1o4  5294  fvun2  5380  fvco2  5382  fvopab3ig  5387  fvpr2  5450  fnopovb  5557  ov  5595  ovigg  5596  ovg  5601  oprssdm  5612  brcupg  5814  braddcfn  5826  fnsex  5832  brcrossg  5848  brpw1fn  5854  brfullfung  5865  brfullfunop  5867  dfnnc3  5885  map0  6025  eqtc  6161  brtcfn  6246  nnc3n3p1  6278  nnc3n3p2  6279  nchoicelem14  6302  fnfreclem2  6318  fnfreclem3  6319