Theorem eqeq1i 2095

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 2094	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 7	1 |- ( A = C <-> B = C )

Syntax hints:   <-> wb 103   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  ssequn2  3173  dfss1  3204  disj  3331  disjr  3332  undisj1  3340  undisj2  3341  uneqdifeqim  3368  reusn  3513  rabsneu  3515  eusn  3516  iin0r  4004  opeqsn  4079  unisuc  4240  onsucelsucexmid  4346  sucprcreg  4365  onintexmid  4388  dmopab3  4649  dm0rn0  4653  ssdmres  4735  imadisj  4794  args  4801  intirr  4818  dminxp  4875  dfrel3  4888  fntpg  5070  fncnv  5080  f0rn0  5205  dff1o4  5261  dffv4g  5302  fvun2  5371  fnreseql  5409  riota1  5626  riota2df  5628  fnotovb  5692  ovid  5761  ov  5764  ovg  5783  f1od2  6000  frec0g  6162  diffitest  6603  prarloclem5  7059  renegcl  7743  elznn0  8765  hashunlem  10212  maxclpr  10655  ex-ceil  11653  nninfsellemqall  11907  nninfomni  11911