Theorem eqeq1i 2088

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

Syntax hints:   <-> wb 103   = wceq 1284

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

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

This theorem is referenced by:  ssequn2  3145  dfss1  3170  disj  3292  disjr  3293  undisj1  3301  undisj2  3302  uneqdifeqim  3328  reusn  3463  rabsneu  3465  eusn  3466  iin0r  3943  opeqsn  4007  unisuc  4168  onsucelsucexmid  4273  sucprcreg  4292  onintexmid  4315  dmopab3  4566  dm0rn0  4570  ssdmres  4651  imadisj  4707  args  4714  intirr  4731  dminxp  4785  dfrel3  4798  fntpg  4975  fncnv  4985  dff1o4  5154  dffv4g  5195  fvun2  5261  fnreseql  5298  riota1  5506  riota2df  5508  fnotovb  5568  ovid  5637  ov  5640  ovg  5659  f1od2  5876  frec0g  6006  diffitest  6371  prarloclem5  6690  renegcl  7369  elznn0  8366  maxclpr  10108  ex-ceil  10564