Theorem eqeq1i 2213

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

Syntax hints:   <-> wb 105   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  ssequn2  3346  dfss1  3377  disj  3509  disjr  3510  undisj1  3518  undisj2  3519  uneqdifeqim  3546  reusn  3704  rabsneu  3706  eusn  3707  iin0r  4213  opeqsn  4297  unisuc  4460  onsucelsucexmid  4578  sucprcreg  4597  onintexmid  4621  dmopab3  4891  dm0rn0  4895  ssdmres  4981  imadisj  5044  args  5051  intirr  5069  dminxp  5127  dfrel3  5140  fntpg  5330  fncnv  5340  f0rn0  5470  dff1o4  5530  dffv4g  5573  fvun2  5646  fnreseql  5690  funopdmsn  5764  riota1  5918  riota2df  5920  fnotovb  5988  ovid  6062  ov  6065  ovg  6085  f1od2  6321  frec0g  6483  diffitest  6984  ismkvnex  7257  prarloclem5  7613  renegcl  8333  elznn0  9387  seqf1oglem1  10664  seqf1oglem2  10665  hashunlem  10949  maxclpr  11533  gausslemma2d  15546  lgseisenlem1  15547  2lgslem4  15580  ex-ceil  15662  nninfsellemqall  15952  nninfomni  15956  iswomni0  15990