Theorem eqeq1i 2239

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

Syntax hints:   <-> wb 105   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  ssequn2  3382  dfss1  3413  disj  3545  disjr  3546  undisj1  3554  undisj2  3555  uneqdifeqim  3582  reusn  3746  rabsneu  3748  eusn  3749  iin0r  4265  opeqsn  4351  unisuc  4516  onsucelsucexmid  4634  sucprcreg  4653  onintexmid  4677  dmopab3  4950  dm0rn0  4954  ssdmres  5041  imadisj  5105  args  5112  intirr  5130  dminxp  5188  dfrel3  5201  cbviotavw  5299  fntpg  5393  fncnv  5403  f0rn0  5540  dff1o4  5600  dffv4g  5645  fvun2  5722  fnreseql  5766  funopdmsn  5842  riota1  6001  riota2df  6003  riotaeqimp  6006  fnbrovb  6073  fnotovb  6074  ovid  6148  ov  6151  ovg  6171  f1od2  6409  frec0g  6606  diffitest  7119  ismkvnex  7414  prarloclem5  7780  renegcl  8499  elznn0  9555  seqf1oglem1  10844  seqf1oglem2  10845  hashunlem  11130  maxclpr  11862  gausslemma2d  15888  lgseisenlem1  15889  2lgslem4  15922  edg0iedg0g  16007  ushgredgedg  16167  ushgredgedgloop  16169  uhgr0v0e  16175  1loopgrvd2fi  16246  ex-ceil  16440  nninfsellemqall  16741  nninfomni  16745  iswomni0  16784