Theorem eqeq1i 2246

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

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqabb  2374  ssequn2  3402  ineqcom  3422  dfss1  3435  disj  3573  disjr  3574  undisj1  3582  undisj2  3583  uneqdifeqim  3613  reusn  3782  rabsneu  3784  eusn  3785  iin0r  4308  opeqsn  4395  unisuc  4560  onsucelsucexmid  4679  sucprcreg  4698  onintexmid  4722  dmopab3  4996  dm0rn0  5000  ssdmres  5087  imadisj  5152  args  5159  intirr  5177  dminxp  5235  dfrel3  5248  cbviotavw  5346  fntpg  5440  fncnv  5450  fresaunres1disj  5574  f0rn0  5590  dff1o4  5650  dffv4g  5695  fvun2  5773  fnreseql  5822  funopdmsn  5898  riota1  6061  riota2df  6063  riotaeqimp  6066  fnbrovb  6133  fnotovb  6134  ovid  6208  ov  6211  ovg  6231  f1od2  6475  frec0g  6672  diffitest  7195  ismkvnex  7501  prarloclem5  7873  renegcl  8594  addeq0  8710  elznn0  9670  seqf1oglem1  10977  seqf1oglem2  10978  hashunlem  11266  maxclpr  12011  gausslemma2d  16393  lgseisenlem1  16394  2lgslem4  16427  edg0iedg0g  16512  ushgredgedg  16672  ushgredgedgloop  16674  uhgr0v0e  16680  1loopgrvd2fi  16751  ex-ceil  16945  nninfsellemqall  17264  nninfomni  17268  iswomni0  17308