Theorem eqeq1i 2147

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

Syntax hints:   <-> wb 104   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  ssequn2  3249  dfss1  3280  disj  3411  disjr  3412  undisj1  3420  undisj2  3421  uneqdifeqim  3448  reusn  3594  rabsneu  3596  eusn  3597  iin0r  4093  opeqsn  4174  unisuc  4335  onsucelsucexmid  4445  sucprcreg  4464  onintexmid  4487  dmopab3  4752  dm0rn0  4756  ssdmres  4841  imadisj  4901  args  4908  intirr  4925  dminxp  4983  dfrel3  4996  fntpg  5179  fncnv  5189  f0rn0  5317  dff1o4  5375  dffv4g  5418  fvun2  5488  fnreseql  5530  riota1  5748  riota2df  5750  fnotovb  5814  ovid  5887  ov  5890  ovg  5909  f1od2  6132  frec0g  6294  diffitest  6781  ismkvnex  7029  prarloclem5  7308  renegcl  8023  elznn0  9069  hashunlem  10550  maxclpr  10994  ex-ceil  12938  nninfsellemqall  13211  nninfomni  13215