Theorem eqeq1i 2183

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

Syntax hints:   <-> wb 105   = wceq 1353

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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  ssequn2  3306  dfss1  3337  disj  3469  disjr  3470  undisj1  3478  undisj2  3479  uneqdifeqim  3506  reusn  3660  rabsneu  3662  eusn  3663  iin0r  4164  opeqsn  4246  unisuc  4407  onsucelsucexmid  4523  sucprcreg  4542  onintexmid  4566  dmopab3  4833  dm0rn0  4837  ssdmres  4922  imadisj  4983  args  4990  intirr  5007  dminxp  5065  dfrel3  5078  fntpg  5264  fncnv  5274  f0rn0  5402  dff1o4  5461  dffv4g  5504  fvun2  5575  fnreseql  5618  riota1  5839  riota2df  5841  fnotovb  5908  ovid  5981  ov  5984  ovg  6003  f1od2  6226  frec0g  6388  diffitest  6877  ismkvnex  7143  prarloclem5  7474  renegcl  8192  elznn0  9239  hashunlem  10750  maxclpr  11197  ex-ceil  14036  nninfsellemqall  14323  nninfomni  14327  iswomni0  14358