Theorem eqeq2d 2208

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 2206	. 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 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtrd  2229  eq2tri  2256  rspcedeq2vd  2878  rspceeqv  2886  sbceq1g  3104  euabsn  3693  absneu  3695  preq12bg  3804  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  mpteq12f  4114  cbvmptf  4128  cbvmpt  4129  exmidsssn  4236  exmidsssnc  4237  opth  4271  eqvinop  4277  moop2  4285  euotd  4288  eusvnf  4489  reusv3i  4495  nlimsucg  4603  nn0suc  4641  opelxp  4694  elvvv  4727  relop  4817  elrnmpt1s  4917  elrnmpt1  4918  elsnres  4984  elxp4  5158  elxp5  5159  relresfld  5200  iotajust  5219  iota1  5234  iota2df  5245  funopg  5293  funcnvuni  5328  fun11iun  5526  funcocnv2  5530  nfvres  5593  ssimaex  5623  fvmptg  5638  fvmptdf  5650  fvopab6  5659  fnmptfvd  5667  fmptco  5729  fsng  5736  foco2  5801  elabrex  5805  elabrexg  5806  abrexco  5807  f1veqaeq  5817  dff13f  5818  f1ocnvfv  5827  f1ocnvfvb  5828  fcofo  5832  fliftfun  5844  fliftval  5848  f1oiso2  5875  riota5f  5903  oprabid  5955  rspceov  5966  dfoprab2  5971  mpoeq123dva  5985  mpoeq3dva  5988  cbvoprab1  5996  cbvoprab2  5997  cbvoprab12  5998  cbvmpox  6002  mpomptx  6015  ovmpos  6048  ovmpodf  6056  ovmpodv2  6058  ovi3  6062  ov6g  6063  fnrnov  6071  foov  6072  caovcang  6087  caovcan  6090  f1opw2  6131  opabex3d  6180  opabex3  6181  fo1st  6217  fo2nd  6218  elxp6  6229  op1steq  6239  dfoprab4f  6253  fmpox  6260  fnmpoovd  6275  df1st2  6279  df2nd2  6280  xporderlem  6291  cnvoprab  6294  f1od2  6295  brtpos2  6311  dftpos4  6323  tposfn2  6326  recseq  6366  tfr1onlemaccex  6408  tfrcllemaccex  6421  frecabcl  6459  frecsuc  6467  nna0r  6538  eqerlem  6625  qseq2  6645  ecelqsg  6649  snec  6657  qsinxp  6672  ecoptocl  6683  eroveu  6687  th3qlem1  6698  th3qlem2  6699  th3q  6701  mapsncnv  6756  elixpsn  6796  ixpsnf1o  6797  en1  6860  mapsnen  6872  xpsnen  6882  xpassen  6891  pw2f1odclem  6897  xpf1o  6907  mapen  6909  mapxpen  6911  fidifsnen  6933  ac6sfi  6961  undifdc  6987  djuf1olem  7121  djur  7137  updjud  7150  omp1eomlem  7162  0ct  7175  enumctlemm  7182  fodjuomnilemdc  7212  fodjuomni  7217  fodjumkv  7228  nninfwlporlemd  7240  exmidfodomrlemeldju  7269  exmidfodomrlemreseldju  7270  cc2lem  7336  dfplpq2  7424  dfmpq2  7425  enqbreq2  7427  enq0sym  7502  enq0ref  7503  enq0tr  7504  addnq0mo  7517  mulnq0mo  7518  addnnnq0  7519  mulnnnq0  7520  nqnq0a  7524  nqnq0m  7525  nq0a0  7527  prarloclemcalc  7572  genipv  7579  genpassl  7594  genpassu  7595  addcomprg  7648  mulcomprg  7650  distrlem1prl  7652  distrlem1pru  7653  distrlem5prl  7656  distrlem5pru  7657  1idprl  7660  1idpru  7661  recexprlem1ssl  7703  recexprlem1ssu  7704  addsrmo  7813  mulsrmo  7814  addsrpr  7815  mulsrpr  7816  elreal  7898  axcnre  7951  axcaucvglemval  7967  negeu  8220  subeq0  8255  apreap  8617  apreim  8633  divmulap3  8707  diveqap0  8712  diveqap1  8735  nn0ind-raph  9446  elq  9699  zq  9703  elpq  9726  cnref1o  9728  iccf1o  10082  fzen  10121  fseq1m1p1  10173  fzm1  10178  modqmuladd  10461  modqmuladdnn0  10463  modfzo0difsn  10490  nn0ennn  10528  seqf1oglem1  10614  seq3id2  10621  qsqeqor  10745  bcval5  10858  fihashen1  10894  shftlem  10984  shftfvalg  10986  shftfval  10989  negfi  11396  xrmaxiflemcom  11417  xrnegiso  11430  xrnegcon1d  11432  sumeq2  11527  summodc  11551  fsum3  11555  fsum2dlemstep  11602  isumsplit  11659  mertenslemub  11702  mertensabs  11705  prodeq2w  11724  prodeq2  11725  prodmodc  11746  fprodseq  11751  fprod2dlemstep  11790  moddvds  11967  modm1div  11968  dvdsnegb  11976  dvdsabseq  12015  dvdsmod  12030  odd2np1lem  12040  odd2np1  12041  opeo  12065  omeo  12066  divalglemnn  12086  divalglemeunn  12089  divalglemex  12090  divalglemeuneg  12091  bitsinv1lem  12129  bezoutlemnewy  12174  bezoutlema  12177  bezoutlemb  12178  bezoutlemex  12179  bezoutlemaz  12181  bezoutlembz  12182  eucalglt  12236  qredeq  12275  qredeu  12276  divgcdcoprm0  12280  divgcdcoprmex  12281  cncongr1  12282  cncongr2  12283  qnumdenbi  12371  hashgcdlem  12417  coprimeprodsq2  12438  pythagtriplem18  12461  pythagtriplem19  12462  pceu  12475  pcval  12476  pczpre  12477  pcdiv  12482  dvdsprmpweq  12515  dvdsprmpweqnn  12516  difsqpwdvds  12518  pcmpt  12523  pcfac  12530  oddprmdvds  12534  4sqlem2  12569  4sqlem3  12570  4sqlem4  12572  4sqlem12  12582  evenennn  12621  ennnfonelemim  12652  ptex  12952  intopsn  13036  igsumvalx  13058  gsumfzval  13060  gsumpropd  13061  gsumpropd2  13062  gsumress  13064  gsumval2  13066  ismnddef  13085  sgrpidmndm  13087  mndpfo  13105  mhmex  13120  grpid  13197  grpidrcan  13223  grpidlcan  13224  grplactcnv  13260  isghm  13399  f1ghm0to0  13428  conjghm  13432  srgpcomp  13572  ringadd2  13609  rrgval  13844  opprdomnbg  13856  islmod  13873  lss1d  13965  rspsn  14116  expghmap  14189  zndvds0  14232  znf1o  14233  istopon  14275  eltg3  14319  restsn  14442  txuni2  14518  txopn  14527  upxp  14534  uptx  14536  txrest  14538  hmeoimaf1o  14576  xmettxlem  14771  xmettx  14772  elply2  14997  elplyr  15002  dvdsppwf1o  15251  mpodvdsmulf1o  15252  perfectlem2  15262  perfect  15263  lgslem1  15267  lgsdirnn0  15314  lgsdinn0  15315  gausslemma2dlem0i  15324  gausslemma2dlem1a  15325  gausslemma2d  15336  lgseisenlem2  15338  lgsquadlem2  15345  2lgslem1b  15356  2lgslem3a1  15364  2lgslem3b1  15365  2lgslem3c1  15366  2lgslem3d1  15367  2lgsoddprmlem2  15373  2sqlem2  15382  2sqlem8  15390  2sqlem9  15391  bj-nn0suc0  15622  bj-inf2vnlem1  15642  bj-nn0sucALT  15650  pwle2  15669  iooref1o  15705