Theorem eqeq1i 2242

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 2241	. 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 2216

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

This theorem is referenced by:  eqabb  2370  ssequn2  3394  ineqcom  3414  dfss1  3427  disj  3559  disjr  3560  undisj1  3568  undisj2  3569  uneqdifeqim  3597  reusn  3764  rabsneu  3766  eusn  3767  iin0r  4284  opeqsn  4371  unisuc  4536  onsucelsucexmid  4654  sucprcreg  4673  onintexmid  4697  dmopab3  4971  dm0rn0  4975  ssdmres  5062  imadisj  5126  args  5133  intirr  5151  dminxp  5209  dfrel3  5222  cbviotavw  5320  fntpg  5414  fncnv  5424  fresaunres1disj  5548  f0rn0  5564  dff1o4  5624  dffv4g  5669  fvun2  5746  fnreseql  5790  funopdmsn  5866  riota1  6025  riota2df  6027  riotaeqimp  6030  fnbrovb  6097  fnotovb  6098  ovid  6172  ov  6175  ovg  6195  f1od2  6433  frec0g  6630  diffitest  7146  ismkvnex  7448  prarloclem5  7817  renegcl  8536  elznn0  9594  seqf1oglem1  10885  seqf1oglem2  10886  hashunlem  11172  maxclpr  11911  gausslemma2d  15959  lgseisenlem1  15960  2lgslem4  15993  edg0iedg0g  16078  ushgredgedg  16238  ushgredgedgloop  16240  uhgr0v0e  16246  1loopgrvd2fi  16317  ex-ceil  16511  nninfsellemqall  16810  nninfomni  16814  iswomni0  16853