Theorem eqeq1i 2213

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 2212	. 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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  ssequn2  3346  dfss1  3377  disj  3509  disjr  3510  undisj1  3518  undisj2  3519  uneqdifeqim  3546  reusn  3704  rabsneu  3706  eusn  3707  iin0r  4214  opeqsn  4298  unisuc  4461  onsucelsucexmid  4579  sucprcreg  4598  onintexmid  4622  dmopab3  4892  dm0rn0  4896  ssdmres  4982  imadisj  5045  args  5052  intirr  5070  dminxp  5128  dfrel3  5141  fntpg  5331  fncnv  5341  f0rn0  5472  dff1o4  5532  dffv4g  5575  fvun2  5648  fnreseql  5692  funopdmsn  5766  riota1  5920  riota2df  5922  fnotovb  5990  ovid  6064  ov  6067  ovg  6087  f1od2  6323  frec0g  6485  diffitest  6986  ismkvnex  7259  prarloclem5  7615  renegcl  8335  elznn0  9389  seqf1oglem1  10666  seqf1oglem2  10667  hashunlem  10951  maxclpr  11566  gausslemma2d  15579  lgseisenlem1  15580  2lgslem4  15613  edg0iedg0g  15693  ex-ceil  15699  nninfsellemqall  15989  nninfomni  15993  iswomni0  16027