Theorem eqeq2i 1477

Description: Inference from equality to equivalence of equalities.

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

Syntax hints:   <-> wb 146   = wceq 953

This theorem is referenced by:  eqeq12i 1480  eqtr 1487  rabid2 1762  dfss2 2048  ssequn1 2190  preq12b 2474  preqsn 2477  pwex 2735  opprc3 2787  opeqpr 2792  wefrc 2933  orddif 3065  onuninsuc 3098  funopg 3533  funimaexg 3561  fnressn 3822  fressnfv 3823  fvresex 3842  abrexexlem2 3844  dfrdg2 3918  rdgsucopab 3931  rdgsucopabn 3932  frsucopab 3939  fnoprval 4002  elxp6 4086  eqerlem 4254  qsid 4285  pwfi 4545  rankr1 4646  ac6lem 4726  cardeq0 4804  card1 4805  cf0 4882  addcompr 5095  mulcompr 5097  axrnegex 5255  axrrecex 5256  pnfnemnf 5509  mul0or 5663  muleqaddt 5669  dfnn2 5884  sqr00t 6644  sqr2irrlem4 6657  cjreb 6716  cjne0t 6766  fsumser0f 6939  fsumser1f 6940  binomlem6 7009  reeff1o 7368  subtop 7588  sn0top 7589  ismet 7737  dfms2 7738  msflem 7742  oprcn 7911  fsumcnlem 7923  isgrp 7975  ringi 8079  vci 8104  spwval2 8577  efifolem2 8638  efifolem6 8642  chnle 9323  h1de2ctlem 9394  cmcmlem 9451  cmcm2 9453  cmbr2 9456  osumcor2 9507  pjss2 9542  ho01 9671  nmop0h 9831  pjclem1 10033  jplem1 10105  atabs2 10237  cdj3lem3 10270  cdj3lem3b 10272  cayleylem3 10318  fine 10348  isalg 10497  algi 10504  dedi 10514  cati 10532  hgralem 10606

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain