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  3437  dfss1  3461  dfss4  3490  disjr  3593  undisj1  3603  undisj2  3604  undif  3631  uneqdifeq  3639  reusn  3794  rabsneu  3796  eusn  3797  uniintsn  3964  dfiota4  4373  dfaddc2  4382  addccom  4407  addcass  4416  nndisjeq  4430  vfin1cltv  4548  phidisjnn  4616  opeqexb  4621  dmopab3  4918  dm0rn0  4922  ssdmres  4988  resabs1  4993  imadisj  5016  intirr  5030  dminxp  5062  funun  5147  fncnv  5159  dff1o4  5295  fvun2  5381  fvco2  5383  fvopab3ig  5388  fvpr2  5451  fnopovb  5558  ov  5596  ovigg  5597  ovg  5602  oprssdm  5613  brcupg  5815  braddcfn  5827  fnsex  5833  brcrossg  5849  brpw1fn  5855  brfullfung  5866  brfullfunop  5868  dfnnc3  5886  map0  6026  eqtc  6162  brtcfn  6247  nnc3n3p1  6279  nnc3n3p2  6280  nchoicelem14  6303  fnfreclem2  6319  fnfreclem3  6320