Theorem eqeq1i 2201

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

Syntax hints:   <-> wb 105   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  ssequn2  3333  dfss1  3364  disj  3496  disjr  3497  undisj1  3505  undisj2  3506  uneqdifeqim  3533  reusn  3690  rabsneu  3692  eusn  3693  iin0r  4199  opeqsn  4282  unisuc  4445  onsucelsucexmid  4563  sucprcreg  4582  onintexmid  4606  dmopab3  4876  dm0rn0  4880  ssdmres  4965  imadisj  5028  args  5035  intirr  5053  dminxp  5111  dfrel3  5124  fntpg  5311  fncnv  5321  f0rn0  5449  dff1o4  5509  dffv4g  5552  fvun2  5625  fnreseql  5669  riota1  5893  riota2df  5895  fnotovb  5962  ovid  6036  ov  6039  ovg  6059  f1od2  6290  frec0g  6452  diffitest  6945  ismkvnex  7216  prarloclem5  7562  renegcl  8282  elznn0  9335  seqf1oglem1  10593  seqf1oglem2  10594  hashunlem  10878  maxclpr  11369  gausslemma2d  15226  lgseisenlem1  15227  2lgslem4  15260  ex-ceil  15288  nninfsellemqall  15575  nninfomni  15579  iswomni0  15611