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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  ssequn2  3380  dfss1  3411  disj  3543  disjr  3544  undisj1  3552  undisj2  3553  uneqdifeqim  3580  reusn  3742  rabsneu  3744  eusn  3745  iin0r  4259  opeqsn  4345  unisuc  4510  onsucelsucexmid  4628  sucprcreg  4647  onintexmid  4671  dmopab3  4944  dm0rn0  4948  ssdmres  5035  imadisj  5098  args  5105  intirr  5123  dminxp  5181  dfrel3  5194  cbviotavw  5292  fntpg  5386  fncnv  5396  f0rn0  5531  dff1o4  5591  dffv4g  5636  fvun2  5713  fnreseql  5757  funopdmsn  5834  riota1  5991  riota2df  5993  riotaeqimp  5996  fnbrovb  6063  fnotovb  6064  ovid  6138  ov  6141  ovg  6161  f1od2  6400  frec0g  6563  diffitest  7076  ismkvnex  7354  prarloclem5  7720  renegcl  8440  elznn0  9494  seqf1oglem1  10782  seqf1oglem2  10783  hashunlem  11068  maxclpr  11800  gausslemma2d  15817  lgseisenlem1  15818  2lgslem4  15851  edg0iedg0g  15936  ushgredgedg  16096  ushgredgedgloop  16098  uhgr0v0e  16104  1loopgrvd2fi  16175  ex-ceil  16369  nninfsellemqall  16668  nninfomni  16672  iswomni0  16707