Theorem eqeq2d 2106

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq2d.1	|- ( ph -> A = B )

Assertion

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

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 |- ( ph -> A = B )
2		eqeq2 2104	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C = A <-> C = B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088

This theorem is referenced by:  eqtrd  2127  eq2tri  2154  rspcedeq2vd  2745  rspceeqv  2753  sbceq1g  2965  euabsn  3532  absneu  3534  preq12bg  3639  cbvopab  3931  cbvopab1  3933  cbvopab2  3934  cbvopab1s  3935  cbvopab2v  3937  mpteq12f  3940  cbvmptf  3954  cbvmpt  3955  exmidsssn  4055  opth  4088  eqvinop  4094  moop2  4102  euotd  4105  eusvnf  4303  reusv3i  4309  nlimsucg  4410  nn0suc  4447  opelxp  4497  elvvv  4530  relop  4617  elrnmpt1s  4717  elrnmpt1  4718  elsnres  4782  elxp4  4952  elxp5  4953  relresfld  4994  iotajust  5013  iota1  5028  iota2df  5038  funopg  5082  funcnvuni  5117  fun11iun  5309  funcocnv2  5313  nfvres  5372  ssimaex  5400  fvmptg  5415  fvmptdf  5426  fvopab6  5435  fmptco  5503  fsng  5509  foco2  5571  elabrex  5575  abrexco  5576  f1veqaeq  5586  dff13f  5587  f1ocnvfv  5596  f1ocnvfvb  5597  fcofo  5601  fliftfun  5613  fliftval  5617  f1oiso2  5644  riota5f  5670  oprabid  5719  rspceov  5729  dfoprab2  5734  mpt2eq123dva  5748  mpt2eq3dva  5751  cbvoprab1  5758  cbvoprab2  5759  cbvoprab12  5760  cbvmpt2x  5764  mpt2mptx  5777  ovmpt2s  5806  ovmpt2df  5814  ovmpt2dv2  5816  ovi3  5819  ov6g  5820  fnrnov  5828  foov  5829  caovcang  5844  caovcan  5847  f1opw2  5888  opabex3d  5930  opabex3  5931  fo1st  5966  fo2nd  5967  elxp6  5978  op1steq  5987  dfoprab4f  6001  fmpt2x  6008  df1st2  6022  df2nd2  6023  xporderlem  6034  cnvoprab  6037  f1od2  6038  brtpos2  6054  dftpos4  6066  tposfn2  6069  recseq  6109  tfr1onlemaccex  6151  tfrcllemaccex  6164  frecabcl  6202  frecsuc  6210  nna0r  6279  eqerlem  6363  qseq2  6381  ecelqsg  6385  snec  6393  qsinxp  6408  ecoptocl  6419  eroveu  6423  th3qlem1  6434  th3qlem2  6435  th3q  6437  mapsncnv  6492  elixpsn  6532  ixpsnf1o  6533  en1  6596  mapsnen  6608  xpsnen  6617  xpassen  6626  xpf1o  6640  mapen  6642  mapxpen  6644  fidifsnen  6666  ac6sfi  6694  undifdc  6714  djuf1olem  6825  djur  6837  updjud  6853  0ct  6869  enumctlemm  6872  fodjuomnilemdc  6887  fodjuomni  6892  fodjumkv  6903  exmidfodomrlemeldju  6922  exmidfodomrlemreseldju  6923  dfplpq2  7010  dfmpq2  7011  enqbreq2  7013  enq0sym  7088  enq0ref  7089  enq0tr  7090  addnq0mo  7103  mulnq0mo  7104  addnnnq0  7105  mulnnnq0  7106  nqnq0a  7110  nqnq0m  7111  nq0a0  7113  prarloclemcalc  7158  genipv  7165  genpassl  7180  genpassu  7181  addcomprg  7234  mulcomprg  7236  distrlem1prl  7238  distrlem1pru  7239  distrlem5prl  7242  distrlem5pru  7243  1idprl  7246  1idpru  7247  recexprlem1ssl  7289  recexprlem1ssu  7290  addsrmo  7386  mulsrmo  7387  addsrpr  7388  mulsrpr  7389  elreal  7463  axcnre  7513  axcaucvglemval  7529  negeu  7770  subeq0  7805  apreap  8161  apreim  8177  divmulap3  8241  diveqap0  8246  diveqap1  8269  nn0ind-raph  8962  elq  9206  zq  9210  cnref1o  9232  iccf1o  9570  fzen  9606  fseq1m1p1  9658  fzm1  9663  modqmuladd  9922  modqmuladdnn0  9924  modfzo0difsn  9951  nn0ennn  9989  seq3id2  10059  bcval5  10286  fihashen1  10322  shftlem  10365  shftfvalg  10367  shftfval  10370  negfi  10774  xrmaxiflemcom  10792  xrnegiso  10805  xrnegcon1d  10807  sumeq2  10902  summodc  10926  fsum3  10930  fsum2dlemstep  10977  isumsplit  11034  mertenslemub  11077  mertensabs  11080  moddvds  11232  dvdsnegb  11240  dvdsabseq  11275  dvdsmod  11290  odd2np1lem  11299  odd2np1  11300  opeo  11324  omeo  11325  divalglemnn  11345  divalglemeunn  11348  divalglemex  11349  divalglemeuneg  11350  bezoutlemnewy  11412  bezoutlema  11415  bezoutlemb  11416  bezoutlemex  11417  bezoutlemaz  11419  bezoutlembz  11420  eucalglt  11466  qredeq  11505  qredeu  11506  divgcdcoprm0  11510  divgcdcoprmex  11511  cncongr1  11512  cncongr2  11513  qnumdenbi  11597  hashgcdlem  11630  evenennn  11633  istopon  11864  eltg3  11909  restsn  12032  bj-nn0suc0  12553  bj-inf2vnlem1  12573  bj-nn0sucALT  12581