Theorem eqeq2d 2243

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 2241	. 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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtrd  2264  eq2tri  2291  rspcedeq2vd  2920  rspceeqv  2928  sbceq1g  3147  euabsn  3741  absneu  3743  ifpprsnssdc  3779  preq12bg  3856  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  mpteq12f  4169  cbvmptf  4183  cbvmpt  4184  exmidsssn  4292  exmidsssnc  4293  opth  4329  eqvinop  4335  moop2  4344  euotd  4347  eusvnf  4550  reusv3i  4556  nlimsucg  4664  nn0suc  4702  opelxp  4755  elvvv  4789  relop  4880  elrnmpt1s  4982  elrnmpt1  4983  elsnres  5050  elxp4  5224  elxp5  5225  relresfld  5266  iotajust  5285  iota1  5301  iota2df  5312  funopg  5360  funcnvuni  5399  fun11iun  5604  funcocnv2  5608  nfvres  5675  ssimaex  5707  fvmptg  5722  fvmptdf  5734  fvopab6  5743  fnmptfvd  5751  fmptco  5813  fsng  5820  fsn2g  5822  funopsn  5830  foco2  5894  elabrex  5898  elabrexg  5899  abrexco  5900  f1veqaeq  5910  dff13f  5911  f1ocnvfv  5920  f1ocnvfvb  5921  fcofo  5925  fliftfun  5937  fliftval  5941  f1oiso2  5968  riotaeqimp  5996  riota5f  5998  oprabid  6050  rspceov  6061  dfoprab2  6068  mpoeq123dva  6082  mpoeq3dva  6085  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvmpox  6099  mpomptx  6112  ovmpos  6145  ovmpodf  6153  ovmpodv2  6155  ovi3  6159  ov6g  6160  fnrnov  6168  foov  6169  caovcang  6184  caovcan  6187  f1opw2  6229  opabex3d  6283  opabex3  6284  fo1st  6320  fo2nd  6321  elxp6  6332  op1steq  6342  dfoprab4f  6356  fmpox  6365  fnmpoovd  6380  df1st2  6384  df2nd2  6385  xporderlem  6396  cnvoprab  6399  f1od2  6400  brtpos2  6417  dftpos4  6429  tposfn2  6432  recseq  6472  tfr1onlemaccex  6514  tfrcllemaccex  6527  frecabcl  6565  frecsuc  6573  nna0r  6646  eqerlem  6733  qseq2  6753  ecelqsg  6757  snec  6765  qsinxp  6780  ecoptocl  6791  eroveu  6795  th3qlem1  6806  th3qlem2  6807  th3q  6809  mapsncnv  6864  elixpsn  6904  ixpsnf1o  6905  en1  6973  mapsnen  6986  en2  6998  xpsnen  7005  xpassen  7014  pw2f1odclem  7020  xpf1o  7030  mapen  7032  mapxpen  7034  fidifsnen  7057  ac6sfi  7087  undifdc  7116  djuf1olem  7252  djur  7268  updjud  7281  omp1eomlem  7293  0ct  7306  enumctlemm  7313  fodjuomnilemdc  7343  fodjuomni  7348  fodjumkv  7359  nninfwlporlemd  7371  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  cc2lem  7485  dfplpq2  7574  dfmpq2  7575  enqbreq2  7577  enq0sym  7652  enq0ref  7653  enq0tr  7654  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  nqnq0a  7674  nqnq0m  7675  nq0a0  7677  prarloclemcalc  7722  genipv  7729  genpassl  7744  genpassu  7745  addcomprg  7798  mulcomprg  7800  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  1idprl  7810  1idpru  7811  recexprlem1ssl  7853  recexprlem1ssu  7854  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  elreal  8048  axcnre  8101  axcaucvglemval  8117  negeu  8370  subeq0  8405  apreap  8767  apreim  8783  divmulap3  8857  diveqap0  8862  diveqap1  8885  nn0ind-raph  9597  elq  9856  zq  9860  elpq  9883  cnref1o  9885  iccf1o  10239  fzen  10278  fseq1m1p1  10330  fzm1  10335  modqmuladd  10629  modqmuladdnn0  10631  modfzo0difsn  10658  nn0ennn  10696  seqf1oglem1  10782  seq3id2  10789  qsqeqor  10913  bcval5  11026  fihashen1  11062  wrdl1exs1  11210  wrdl1s1  11211  wrd2ind  11308  swrdccatin2d  11329  reuccatpfxs1lem  11331  shftlem  11394  shftfvalg  11396  shftfval  11399  negfi  11806  xrmaxiflemcom  11827  xrnegiso  11840  xrnegcon1d  11842  sumeq2  11937  summodc  11962  fsum3  11966  fsum2dlemstep  12013  isumsplit  12070  mertenslemub  12113  mertensabs  12116  prodeq2w  12135  prodeq2  12136  prodmodc  12157  fprodseq  12162  fprod2dlemstep  12201  moddvds  12378  modm1div  12379  dvdsnegb  12387  dvdsabseq  12426  dvdsmod  12441  odd2np1lem  12451  odd2np1  12452  opeo  12476  omeo  12477  divalglemnn  12497  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  bitsinv1lem  12540  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  bezoutlemex  12590  bezoutlemaz  12592  bezoutlembz  12593  eucalglt  12647  qredeq  12686  qredeu  12687  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  qnumdenbi  12782  hashgcdlem  12828  coprimeprodsq2  12849  pythagtriplem18  12872  pythagtriplem19  12873  pceu  12886  pcval  12887  pczpre  12888  pcdiv  12893  dvdsprmpweq  12926  dvdsprmpweqnn  12927  difsqpwdvds  12929  pcmpt  12934  pcfac  12941  oddprmdvds  12945  4sqlem2  12980  4sqlem3  12981  4sqlem4  12983  4sqlem12  12993  evenennn  13032  ennnfonelemim  13063  ptex  13365  intopsn  13468  igsumvalx  13490  gsumfzval  13492  gsumpropd  13493  gsumpropd2  13494  gsumress  13496  gsumval2  13498  ismnddef  13519  sgrpidmndm  13521  mndpfo  13539  mhmex  13563  grpid  13640  grpidrcan  13666  grpidlcan  13667  grplactcnv  13703  isghm  13848  f1ghm0to0  13877  conjghm  13881  srgpcomp  14022  ringadd2  14059  rrgval  14295  opprdomnbg  14307  islmod  14324  lss1d  14416  rspsn  14567  expghmap  14640  zndvds0  14683  znf1o  14684  mplvalcoe  14723  istopon  14756  eltg3  14800  restsn  14923  txuni2  14999  txopn  15008  upxp  15015  uptx  15017  txrest  15019  hmeoimaf1o  15057  xmettxlem  15252  xmettx  15253  elply2  15478  elplyr  15483  dvdsppwf1o  15732  mpodvdsmulf1o  15733  perfectlem2  15743  perfect  15744  lgslem1  15748  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  gausslemma2d  15817  lgseisenlem2  15819  lgsquadlem2  15826  2lgslem1b  15837  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  2lgsoddprmlem2  15854  2sqlem2  15863  2sqlem8  15871  2sqlem9  15872  incistruhgr  15960  upgrex  15973  usgredg4  16085  usgredgreu  16086  uspgredg2vtxeu  16088  uspgredg2v  16091  usgredg2vlem2  16093  usgredg2v  16094  vtxdgfifival  16161  vtxdumgrfival  16168  1loopgrvd2fi  16175  wlk1walkdom  16229  upgriswlkdc  16230  eupth2lem3lem3fi  16340  eupth2fi  16349  bj-nn0suc0  16596  bj-inf2vnlem1  16616  bj-nn0sucALT  16624  pwle2  16650  iooref1o  16689  qdiff  16704  gfsumval  16732