Theorem eqeq2i 1731

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

Syntax hints:   <-> wb 162   = wceq 1136

This theorem is referenced by:  eqeq12iOLD 1735  eqtri 1745  rabid2 2087  rabid2OLD 2088  dfss2 2443  ssequn1OLD 2606  preq12b 2976  preqsn 2979  pwexOLD 3303  opprc3 3358  opeqpr 3365  wefrc 3467  orddif 3575  onuninsuci 3732  funopg 4265  funimaexg 4306  fnressn 4623  fressnfv 4624  fvresex 4644  abrexexlem2 4646  fnoprv 4757  elxp6 4852  dfiota2 4901  dfrdg2 4952  rdgsucopab 4965  rdgsucopabn 4966  frsucopab 4973  eqerlem 5139  qsid 5171  ordtype 5501  rankr1 5594  ac6lem 5712  cardeq0 5778  card1 5779  cf0 5854  addcompr 6071  mulcompr 6073  axrnegex 6232  axrrecex 6233  mul0ori 6678  muleqadd 6685  dfnn2 6914  sqr00 7759  sqr2irrlem4 7772  cjrebi 7826  cjne0 7877  fsumser0fi 8056  fsumser1fi 8057  binomlem6 8126  reeff1o 8486  absefib 8545  efieq1re 8546  subtop 8711  sn0top 8712  ismet 8870  dfms2 8871  msflem 8875  oprcn 9050  fsumcnlem 9062  isgrp 9116  ringi 9261  vci 9294  spwval2 9791  sineq0re 9862  efifolem2 9872  efifolem6 9876  oprab2co 9954  fine 10006  fbunfip 10074  usinuniop 10133  chnlei 10833  h1de2ctlem 10903  cmcmlem 10959  cmcm2i 10961  cmbr2i 10964  osumcor2i 11017  pjss2i 11052  ho01i 11183  nmop0h 11345  pjclem1 11560  jplem1 11632  atabs2i 11766  cdj3lem3 11802  cdj3lem3b 11804  bnj141 12265  bnj168 12288  bnj922 12626  bnj927 12627  bnj1366 12883  bnj543 13061  cayleylem3 13435  mpteqi 13631  frsucopabn 13703  trcllem1 13725  islatalg 14257  rngapm 14456  com2i 14488  vri 14557  sbtpsines 14624  trhom 14697  altretop 14707  isalg 14750  algi 14756  dedi 14766  cati 14784  dualalg 14813  fictblem 15052  fictb 15053  ordtypeOLD 15064  dfcon2 15124  cnconn 15126  2ndcctbss 15160  neibastop2lem4 15204  fclsfnflim 15296  flimfnfcls 15297  opropabco 15394  fdc 15494  ismrer1 15706  phtpycom 15732  pcorevlem 15768  isdivrng1 15791  smprngpr 15882  hgralem 15974  elnev 16086  stb2xpl 16501  stb3xpl 16502

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1143  ax-17 1155  ax-4 1157  ax-5o 1159  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-an 241  df-cleq 1714

Copyright terms: Public domain