Theorem eqeq1i 2237

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

Syntax hints:   <-> wb 105   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  ssequn2  3377  dfss1  3408  disj  3540  disjr  3541  undisj1  3549  undisj2  3550  uneqdifeqim  3577  reusn  3737  rabsneu  3739  eusn  3740  iin0r  4253  opeqsn  4339  unisuc  4504  onsucelsucexmid  4622  sucprcreg  4641  onintexmid  4665  dmopab3  4936  dm0rn0  4940  ssdmres  5027  imadisj  5090  args  5097  intirr  5115  dminxp  5173  dfrel3  5186  cbviotavw  5284  fntpg  5377  fncnv  5387  f0rn0  5520  dff1o4  5580  dffv4g  5624  fvun2  5701  fnreseql  5745  funopdmsn  5819  riota1  5974  riota2df  5976  riotaeqimp  5979  fnbrovb  6046  fnotovb  6047  ovid  6121  ov  6124  ovg  6144  f1od2  6381  frec0g  6543  diffitest  7049  ismkvnex  7322  prarloclem5  7687  renegcl  8407  elznn0  9461  seqf1oglem1  10741  seqf1oglem2  10742  hashunlem  11026  maxclpr  11733  gausslemma2d  15748  lgseisenlem1  15749  2lgslem4  15782  edg0iedg0g  15866  ushgredgedg  16024  ushgredgedgloop  16026  ex-ceil  16090  nninfsellemqall  16381  nninfomni  16385  iswomni0  16419