Theorem eqeq2d 2241

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 2239	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C = A <-> C = B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtrd  2262  eq2tri  2289  rspcedeq2vd  2917  rspceeqv  2925  sbceq1g  3144  euabsn  3736  absneu  3738  ifpprsnssdc  3774  preq12bg  3851  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  mpteq12f  4164  cbvmptf  4178  cbvmpt  4179  exmidsssn  4286  exmidsssnc  4287  opth  4323  eqvinop  4329  moop2  4338  euotd  4341  eusvnf  4544  reusv3i  4550  nlimsucg  4658  nn0suc  4696  opelxp  4749  elvvv  4782  relop  4872  elrnmpt1s  4974  elrnmpt1  4975  elsnres  5042  elxp4  5216  elxp5  5217  relresfld  5258  iotajust  5277  iota1  5293  iota2df  5304  funopg  5352  funcnvuni  5390  fun11iun  5595  funcocnv2  5599  nfvres  5665  ssimaex  5697  fvmptg  5712  fvmptdf  5724  fvopab6  5733  fnmptfvd  5741  fmptco  5803  fsng  5810  funopsn  5819  foco2  5883  elabrex  5887  elabrexg  5888  abrexco  5889  f1veqaeq  5899  dff13f  5900  f1ocnvfv  5909  f1ocnvfvb  5910  fcofo  5914  fliftfun  5926  fliftval  5930  f1oiso2  5957  riotaeqimp  5985  riota5f  5987  oprabid  6039  rspceov  6050  dfoprab2  6057  mpoeq123dva  6071  mpoeq3dva  6074  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvmpox  6088  mpomptx  6101  ovmpos  6134  ovmpodf  6142  ovmpodv2  6144  ovi3  6148  ov6g  6149  fnrnov  6157  foov  6158  caovcang  6173  caovcan  6176  f1opw2  6218  opabex3d  6272  opabex3  6273  fo1st  6309  fo2nd  6310  elxp6  6321  op1steq  6331  dfoprab4f  6345  fmpox  6352  fnmpoovd  6367  df1st2  6371  df2nd2  6372  xporderlem  6383  cnvoprab  6386  f1od2  6387  brtpos2  6403  dftpos4  6415  tposfn2  6418  recseq  6458  tfr1onlemaccex  6500  tfrcllemaccex  6513  frecabcl  6551  frecsuc  6559  nna0r  6632  eqerlem  6719  qseq2  6739  ecelqsg  6743  snec  6751  qsinxp  6766  ecoptocl  6777  eroveu  6781  th3qlem1  6792  th3qlem2  6793  th3q  6795  mapsncnv  6850  elixpsn  6890  ixpsnf1o  6891  en1  6959  mapsnen  6972  en2  6981  xpsnen  6988  xpassen  6997  pw2f1odclem  7003  xpf1o  7013  mapen  7015  mapxpen  7017  fidifsnen  7040  ac6sfi  7068  undifdc  7097  djuf1olem  7231  djur  7247  updjud  7260  omp1eomlem  7272  0ct  7285  enumctlemm  7292  fodjuomnilemdc  7322  fodjuomni  7327  fodjumkv  7338  nninfwlporlemd  7350  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  cc2lem  7463  dfplpq2  7552  dfmpq2  7553  enqbreq2  7555  enq0sym  7630  enq0ref  7631  enq0tr  7632  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  nqnq0a  7652  nqnq0m  7653  nq0a0  7655  prarloclemcalc  7700  genipv  7707  genpassl  7722  genpassu  7723  addcomprg  7776  mulcomprg  7778  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  1idprl  7788  1idpru  7789  recexprlem1ssl  7831  recexprlem1ssu  7832  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  elreal  8026  axcnre  8079  axcaucvglemval  8095  negeu  8348  subeq0  8383  apreap  8745  apreim  8761  divmulap3  8835  diveqap0  8840  diveqap1  8863  nn0ind-raph  9575  elq  9829  zq  9833  elpq  9856  cnref1o  9858  iccf1o  10212  fzen  10251  fseq1m1p1  10303  fzm1  10308  modqmuladd  10600  modqmuladdnn0  10602  modfzo0difsn  10629  nn0ennn  10667  seqf1oglem1  10753  seq3id2  10760  qsqeqor  10884  bcval5  10997  fihashen1  11033  wrdl1exs1  11177  wrdl1s1  11178  wrd2ind  11271  swrdccatin2d  11292  reuccatpfxs1lem  11294  shftlem  11343  shftfvalg  11345  shftfval  11348  negfi  11755  xrmaxiflemcom  11776  xrnegiso  11789  xrnegcon1d  11791  sumeq2  11886  summodc  11910  fsum3  11914  fsum2dlemstep  11961  isumsplit  12018  mertenslemub  12061  mertensabs  12064  prodeq2w  12083  prodeq2  12084  prodmodc  12105  fprodseq  12110  fprod2dlemstep  12149  moddvds  12326  modm1div  12327  dvdsnegb  12335  dvdsabseq  12374  dvdsmod  12389  odd2np1lem  12399  odd2np1  12400  opeo  12424  omeo  12425  divalglemnn  12445  divalglemeunn  12448  divalglemex  12449  divalglemeuneg  12450  bitsinv1lem  12488  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  bezoutlemex  12538  bezoutlemaz  12540  bezoutlembz  12541  eucalglt  12595  qredeq  12634  qredeu  12635  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  qnumdenbi  12730  hashgcdlem  12776  coprimeprodsq2  12797  pythagtriplem18  12820  pythagtriplem19  12821  pceu  12834  pcval  12835  pczpre  12836  pcdiv  12841  dvdsprmpweq  12874  dvdsprmpweqnn  12875  difsqpwdvds  12877  pcmpt  12882  pcfac  12889  oddprmdvds  12893  4sqlem2  12928  4sqlem3  12929  4sqlem4  12931  4sqlem12  12941  evenennn  12980  ennnfonelemim  13011  ptex  13313  intopsn  13416  igsumvalx  13438  gsumfzval  13440  gsumpropd  13441  gsumpropd2  13442  gsumress  13444  gsumval2  13446  ismnddef  13467  sgrpidmndm  13469  mndpfo  13487  mhmex  13511  grpid  13588  grpidrcan  13614  grpidlcan  13615  grplactcnv  13651  isghm  13796  f1ghm0to0  13825  conjghm  13829  srgpcomp  13969  ringadd2  14006  rrgval  14242  opprdomnbg  14254  islmod  14271  lss1d  14363  rspsn  14514  expghmap  14587  zndvds0  14630  znf1o  14631  mplvalcoe  14670  istopon  14703  eltg3  14747  restsn  14870  txuni2  14946  txopn  14955  upxp  14962  uptx  14964  txrest  14966  hmeoimaf1o  15004  xmettxlem  15199  xmettx  15200  elply2  15425  elplyr  15430  dvdsppwf1o  15679  mpodvdsmulf1o  15680  perfectlem2  15690  perfect  15691  lgslem1  15695  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2d  15764  lgseisenlem2  15766  lgsquadlem2  15773  2lgslem1b  15784  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  2lgsoddprmlem2  15801  2sqlem2  15810  2sqlem8  15818  2sqlem9  15819  incistruhgr  15906  upgrex  15919  usgredg4  16029  usgredgreu  16030  uspgredg2vtxeu  16032  uspgredg2v  16035  usgredg2vlem2  16037  usgredg2v  16038  vtxdgfifival  16051  vtxdumgrfival  16058  wlk1walkdom  16105  upgriswlkdc  16106  bj-nn0suc0  16396  bj-inf2vnlem1  16416  bj-nn0sucALT  16424  pwle2  16451  iooref1o  16490