Theorem eqeq2i 2050

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	|- A = B

Assertion

Ref	Expression
eqeq2i	|- ( C = A <-> C = B )

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 |- A = B
2		eqeq2 2049	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	ax-mp 7	1 |- ( C = A <-> C = B )

Syntax hints:   <-> wb 98   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  eqtri  2060  rabid2  2486  dfss2  2934  equncom  3088  preq12b  3541  preqsn  3546  opeqpr  3990  orddif  4271  dfrel4v  4772  dfiota2  4868  funopg  4934  fnressn  5349  fressnfv  5350  acexmidlemph  5505  fnovim  5609  tpossym  5891  tfr0  5937  qsid  6171  recidpirq  6934  axprecex  6954  negeq0  7265  muleqadd  7649  cjne0  9508  sqrt00  9638  sqrtmsq2i  9731