Theorem eqeq1i 2215

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

Syntax hints:   <-> wb 105   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  ssequn2  3354  dfss1  3385  disj  3517  disjr  3518  undisj1  3526  undisj2  3527  uneqdifeqim  3554  reusn  3714  rabsneu  3716  eusn  3717  iin0r  4229  opeqsn  4315  unisuc  4478  onsucelsucexmid  4596  sucprcreg  4615  onintexmid  4639  dmopab3  4910  dm0rn0  4914  ssdmres  5000  imadisj  5063  args  5070  intirr  5088  dminxp  5146  dfrel3  5159  fntpg  5349  fncnv  5359  f0rn0  5492  dff1o4  5552  dffv4g  5596  fvun2  5669  fnreseql  5713  funopdmsn  5787  riota1  5941  riota2df  5943  fnotovb  6011  ovid  6085  ov  6088  ovg  6108  f1od2  6344  frec0g  6506  diffitest  7010  ismkvnex  7283  prarloclem5  7648  renegcl  8368  elznn0  9422  seqf1oglem1  10701  seqf1oglem2  10702  hashunlem  10986  maxclpr  11648  gausslemma2d  15661  lgseisenlem1  15662  2lgslem4  15695  edg0iedg0g  15777  ex-ceil  15862  nninfsellemqall  16154  nninfomni  16158  iswomni0  16192