Theorem eqeq1i 2089

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

Syntax hints:   <-> wb 103   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  ssequn2  3146  dfss1  3177  disj  3299  disjr  3300  undisj1  3308  undisj2  3309  uneqdifeqim  3335  reusn  3471  rabsneu  3473  eusn  3474  iin0r  3951  opeqsn  4015  unisuc  4176  onsucelsucexmid  4281  sucprcreg  4300  onintexmid  4323  dmopab3  4576  dm0rn0  4580  ssdmres  4661  imadisj  4717  args  4724  intirr  4741  dminxp  4795  dfrel3  4808  fntpg  4986  fncnv  4996  dff1o4  5165  dffv4g  5206  fvun2  5272  fnreseql  5309  riota1  5517  riota2df  5519  fnotovb  5579  ovid  5648  ov  5651  ovg  5670  f1od2  5887  frec0g  6046  diffitest  6421  prarloclem5  6752  renegcl  7436  elznn0  8447  sizeunlem  9828  maxclpr  10246  ex-ceil  10742