Theorem eqeq1i 2172

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

Syntax hints:   <-> wb 104   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  ssequn2  3290  dfss1  3321  disj  3452  disjr  3453  undisj1  3461  undisj2  3462  uneqdifeqim  3489  reusn  3641  rabsneu  3643  eusn  3644  iin0r  4142  opeqsn  4224  unisuc  4385  onsucelsucexmid  4501  sucprcreg  4520  onintexmid  4544  dmopab3  4811  dm0rn0  4815  ssdmres  4900  imadisj  4960  args  4967  intirr  4984  dminxp  5042  dfrel3  5055  fntpg  5238  fncnv  5248  f0rn0  5376  dff1o4  5434  dffv4g  5477  fvun2  5547  fnreseql  5589  riota1  5810  riota2df  5812  fnotovb  5876  ovid  5949  ov  5952  ovg  5971  f1od2  6194  frec0g  6356  diffitest  6844  ismkvnex  7110  prarloclem5  7432  renegcl  8150  elznn0  9197  hashunlem  10706  maxclpr  11150  ex-ceil  13444  nninfsellemqall  13729  nninfomni  13733  iswomni0  13764