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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  eqtrd  2264  eq2tri  2291  rspcedeq2vd  2921  rspceeqv  2929  sbceq1g  3148  euabsn  3745  absneu  3747  ifpprsnssdc  3783  preq12bg  3861  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  mpteq12f  4174  cbvmptf  4188  cbvmpt  4189  exmidsssn  4298  exmidsssnc  4299  opth  4335  eqvinop  4341  moop2  4350  euotd  4353  eusvnf  4556  reusv3i  4562  nlimsucg  4670  nn0suc  4708  opelxp  4761  elvvv  4795  relop  4886  elrnmpt1s  4988  elrnmpt1  4989  elsnres  5056  elxp4  5231  elxp5  5232  relresfld  5273  iotajust  5292  iota1  5308  iota2df  5319  funopg  5367  funcnvuni  5406  fun11iun  5613  funcocnv2  5617  nfvres  5684  ssimaex  5716  fvmptg  5731  fvmptdf  5743  fvopab6  5752  fnmptfvd  5760  fmptco  5821  fsng  5828  fsn2g  5830  funopsn  5838  foco2  5904  elabrex  5908  elabrexg  5909  abrexco  5910  f1veqaeq  5920  dff13f  5921  f1ocnvfv  5930  f1ocnvfvb  5931  fcofo  5935  fliftfun  5947  fliftval  5951  f1oiso2  5978  riotaeqimp  6006  riota5f  6008  oprabid  6060  rspceov  6071  dfoprab2  6078  mpoeq123dva  6092  mpoeq3dva  6095  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvmpox  6109  mpomptx  6122  ovmpos  6155  ovmpodf  6163  ovmpodv2  6165  ovi3  6169  ov6g  6170  fnrnov  6178  foov  6179  caovcang  6194  caovcan  6197  f1opw2  6239  opabex3d  6292  opabex3  6293  fo1st  6329  fo2nd  6330  elxp6  6341  op1steq  6351  dfoprab4f  6365  fmpox  6374  fnmpoovd  6389  df1st2  6393  df2nd2  6394  xporderlem  6405  cnvoprab  6408  f1od2  6409  brtpos2  6460  dftpos4  6472  tposfn2  6475  recseq  6515  tfr1onlemaccex  6557  tfrcllemaccex  6570  frecabcl  6608  frecsuc  6616  nna0r  6689  eqerlem  6776  qseq2  6796  ecelqsg  6800  snec  6808  qsinxp  6823  ecoptocl  6834  eroveu  6838  th3qlem1  6849  th3qlem2  6850  th3q  6852  mapsncnv  6907  elixpsn  6947  ixpsnf1o  6948  en1  7016  mapsnen  7029  en2  7041  xpsnen  7048  xpassen  7057  pw2f1odclem  7063  xpf1o  7073  mapen  7075  mapxpen  7077  fidifsnen  7100  ac6sfi  7130  undifdc  7159  djuf1olem  7312  djur  7328  updjud  7341  omp1eomlem  7353  0ct  7366  enumctlemm  7373  fodjuomnilemdc  7403  fodjuomni  7408  fodjumkv  7419  nninfwlporlemd  7431  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  cc2lem  7545  dfplpq2  7634  dfmpq2  7635  enqbreq2  7637  enq0sym  7712  enq0ref  7713  enq0tr  7714  addnq0mo  7727  mulnq0mo  7728  addnnnq0  7729  mulnnnq0  7730  nqnq0a  7734  nqnq0m  7735  nq0a0  7737  prarloclemcalc  7782  genipv  7789  genpassl  7804  genpassu  7805  addcomprg  7858  mulcomprg  7860  distrlem1prl  7862  distrlem1pru  7863  distrlem5prl  7866  distrlem5pru  7867  1idprl  7870  1idpru  7871  recexprlem1ssl  7913  recexprlem1ssu  7914  addsrmo  8023  mulsrmo  8024  addsrpr  8025  mulsrpr  8026  elreal  8108  axcnre  8161  axcaucvglemval  8177  negeu  8429  subeq0  8464  apreap  8826  apreim  8842  divmulap3  8916  diveqap0  8921  diveqap1  8944  nn0ind-raph  9658  elq  9917  zq  9921  elpq  9944  cnref1o  9946  iccf1o  10301  fzen  10340  fseq1m1p1  10392  fzm1  10397  modqmuladd  10691  modqmuladdnn0  10693  modfzo0difsn  10720  nn0ennn  10758  seqf1oglem1  10844  seq3id2  10851  qsqeqor  10975  bcval5  11088  fihashen1  11124  wrdl1exs1  11272  wrdl1s1  11273  wrd2ind  11370  swrdccatin2d  11391  reuccatpfxs1lem  11393  shftlem  11456  shftfvalg  11458  shftfval  11461  negfi  11868  xrmaxiflemcom  11889  xrnegiso  11902  xrnegcon1d  11904  sumeq2  11999  summodc  12024  fsum3  12028  fsum2dlemstep  12075  isumsplit  12132  mertenslemub  12175  mertensabs  12178  prodeq2w  12197  prodeq2  12198  prodmodc  12219  fprodseq  12224  fprod2dlemstep  12263  moddvds  12440  modm1div  12441  dvdsnegb  12449  dvdsabseq  12488  dvdsmod  12503  odd2np1lem  12513  odd2np1  12514  opeo  12538  omeo  12539  divalglemnn  12559  divalglemeunn  12562  divalglemex  12563  divalglemeuneg  12564  bitsinv1lem  12602  bezoutlemnewy  12647  bezoutlema  12650  bezoutlemb  12651  bezoutlemex  12652  bezoutlemaz  12654  bezoutlembz  12655  eucalglt  12709  qredeq  12748  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  qnumdenbi  12844  hashgcdlem  12890  coprimeprodsq2  12911  pythagtriplem18  12934  pythagtriplem19  12935  pceu  12948  pcval  12949  pczpre  12950  pcdiv  12955  dvdsprmpweq  12988  dvdsprmpweqnn  12989  difsqpwdvds  12991  pcmpt  12996  pcfac  13003  oddprmdvds  13007  4sqlem2  13042  4sqlem3  13043  4sqlem4  13045  4sqlem12  13055  evenennn  13094  ennnfonelemim  13125  ptex  13427  intopsn  13530  igsumvalx  13552  gsumfzval  13554  gsumpropd  13555  gsumpropd2  13556  gsumress  13558  gsumval2  13560  ismnddef  13581  sgrpidmndm  13583  mndpfo  13601  mhmex  13625  grpid  13702  grpidrcan  13728  grpidlcan  13729  grplactcnv  13765  isghm  13910  f1ghm0to0  13939  conjghm  13943  srgpcomp  14084  ringadd2  14121  rrgval  14357  opprdomnbg  14370  islmod  14387  lss1d  14479  rspsn  14630  expghmap  14703  zndvds0  14746  znf1o  14747  psrbagconf1o  14774  mplvalcoe  14791  istopon  14824  eltg3  14868  restsn  14991  txuni2  15067  txopn  15076  upxp  15083  uptx  15085  txrest  15087  hmeoimaf1o  15125  xmettxlem  15320  xmettx  15321  elply2  15546  elplyr  15551  dvdsppwf1o  15803  mpodvdsmulf1o  15804  perfectlem2  15814  perfect  15815  lgslem1  15819  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  gausslemma2d  15888  lgseisenlem2  15890  lgsquadlem2  15897  2lgslem1b  15908  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  2lgsoddprmlem2  15925  2sqlem2  15934  2sqlem8  15942  2sqlem9  15943  incistruhgr  16031  upgrex  16044  usgredg4  16156  usgredgreu  16157  uspgredg2vtxeu  16159  uspgredg2v  16162  usgredg2vlem2  16164  usgredg2v  16165  vtxdgfifival  16232  vtxdumgrfival  16239  1loopgrvd2fi  16246  wlk1walkdom  16300  upgriswlkdc  16301  eupth2lem3lem3fi  16411  eupth2fi  16420  bj-nn0suc0  16666  bj-inf2vnlem1  16686  bj-nn0sucALT  16694  pwle2  16720  iooref1o  16766  qdiff  16781  gfsumval  16809