Theorem eqeq2d 2205

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 2203	. 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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtrd  2226  eq2tri  2253  rspcedeq2vd  2875  rspceeqv  2883  sbceq1g  3101  euabsn  3689  absneu  3691  preq12bg  3800  cbvopab  4101  cbvopab1  4103  cbvopab2  4104  cbvopab1s  4105  cbvopab2v  4107  mpteq12f  4110  cbvmptf  4124  cbvmpt  4125  exmidsssn  4232  exmidsssnc  4233  opth  4267  eqvinop  4273  moop2  4281  euotd  4284  eusvnf  4485  reusv3i  4491  nlimsucg  4599  nn0suc  4637  opelxp  4690  elvvv  4723  relop  4813  elrnmpt1s  4913  elrnmpt1  4914  elsnres  4980  elxp4  5154  elxp5  5155  relresfld  5196  iotajust  5215  iota1  5230  iota2df  5241  funopg  5289  funcnvuni  5324  fun11iun  5522  funcocnv2  5526  nfvres  5589  ssimaex  5619  fvmptg  5634  fvmptdf  5646  fvopab6  5655  fnmptfvd  5663  fmptco  5725  fsng  5732  foco2  5797  elabrex  5801  elabrexg  5802  abrexco  5803  f1veqaeq  5813  dff13f  5814  f1ocnvfv  5823  f1ocnvfvb  5824  fcofo  5828  fliftfun  5840  fliftval  5844  f1oiso2  5871  riota5f  5899  oprabid  5951  rspceov  5961  dfoprab2  5966  mpoeq123dva  5980  mpoeq3dva  5983  cbvoprab1  5991  cbvoprab2  5992  cbvoprab12  5993  cbvmpox  5997  mpomptx  6010  ovmpos  6043  ovmpodf  6051  ovmpodv2  6053  ovi3  6057  ov6g  6058  fnrnov  6066  foov  6067  caovcang  6082  caovcan  6085  f1opw2  6126  opabex3d  6175  opabex3  6176  fo1st  6212  fo2nd  6213  elxp6  6224  op1steq  6234  dfoprab4f  6248  fmpox  6255  fnmpoovd  6270  df1st2  6274  df2nd2  6275  xporderlem  6286  cnvoprab  6289  f1od2  6290  brtpos2  6306  dftpos4  6318  tposfn2  6321  recseq  6361  tfr1onlemaccex  6403  tfrcllemaccex  6416  frecabcl  6454  frecsuc  6462  nna0r  6533  eqerlem  6620  qseq2  6640  ecelqsg  6644  snec  6652  qsinxp  6667  ecoptocl  6678  eroveu  6682  th3qlem1  6693  th3qlem2  6694  th3q  6696  mapsncnv  6751  elixpsn  6791  ixpsnf1o  6792  en1  6855  mapsnen  6867  xpsnen  6877  xpassen  6886  pw2f1odclem  6892  xpf1o  6902  mapen  6904  mapxpen  6906  fidifsnen  6928  ac6sfi  6956  undifdc  6982  djuf1olem  7114  djur  7130  updjud  7143  omp1eomlem  7155  0ct  7168  enumctlemm  7175  fodjuomnilemdc  7205  fodjuomni  7210  fodjumkv  7221  nninfwlporlemd  7233  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  cc2lem  7328  dfplpq2  7416  dfmpq2  7417  enqbreq2  7419  enq0sym  7494  enq0ref  7495  enq0tr  7496  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  nqnq0a  7516  nqnq0m  7517  nq0a0  7519  prarloclemcalc  7564  genipv  7571  genpassl  7586  genpassu  7587  addcomprg  7640  mulcomprg  7642  distrlem1prl  7644  distrlem1pru  7645  distrlem5prl  7648  distrlem5pru  7649  1idprl  7652  1idpru  7653  recexprlem1ssl  7695  recexprlem1ssu  7696  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  elreal  7890  axcnre  7943  axcaucvglemval  7959  negeu  8212  subeq0  8247  apreap  8608  apreim  8624  divmulap3  8698  diveqap0  8703  diveqap1  8726  nn0ind-raph  9437  elq  9690  zq  9694  elpq  9717  cnref1o  9719  iccf1o  10073  fzen  10112  fseq1m1p1  10164  fzm1  10169  modqmuladd  10440  modqmuladdnn0  10442  modfzo0difsn  10469  nn0ennn  10507  seqf1oglem1  10593  seq3id2  10600  qsqeqor  10724  bcval5  10837  fihashen1  10873  shftlem  10963  shftfvalg  10965  shftfval  10968  negfi  11374  xrmaxiflemcom  11395  xrnegiso  11408  xrnegcon1d  11410  sumeq2  11505  summodc  11529  fsum3  11533  fsum2dlemstep  11580  isumsplit  11637  mertenslemub  11680  mertensabs  11683  prodeq2w  11702  prodeq2  11703  prodmodc  11724  fprodseq  11729  fprod2dlemstep  11768  moddvds  11945  modm1div  11946  dvdsnegb  11954  dvdsabseq  11992  dvdsmod  12007  odd2np1lem  12016  odd2np1  12017  opeo  12041  omeo  12042  divalglemnn  12062  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  bezoutlemex  12141  bezoutlemaz  12143  bezoutlembz  12144  eucalglt  12198  qredeq  12237  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  qnumdenbi  12333  hashgcdlem  12379  coprimeprodsq2  12399  pythagtriplem18  12422  pythagtriplem19  12423  pceu  12436  pcval  12437  pczpre  12438  pcdiv  12443  dvdsprmpweq  12476  dvdsprmpweqnn  12477  difsqpwdvds  12479  pcmpt  12484  pcfac  12491  oddprmdvds  12495  4sqlem2  12530  4sqlem3  12531  4sqlem4  12533  4sqlem12  12543  evenennn  12553  ennnfonelemim  12584  ptex  12878  intopsn  12953  igsumvalx  12975  gsumfzval  12977  gsumpropd  12978  gsumpropd2  12979  gsumress  12981  gsumval2  12983  ismnddef  13002  sgrpidmndm  13004  mndpfo  13022  mhmex  13037  grpid  13114  grpidrcan  13140  grpidlcan  13141  grplactcnv  13177  isghm  13316  f1ghm0to0  13345  conjghm  13349  srgpcomp  13489  ringadd2  13526  rrgval  13761  opprdomnbg  13773  islmod  13790  lss1d  13882  rspsn  14033  expghmap  14106  zndvds0  14149  znf1o  14150  istopon  14192  eltg3  14236  restsn  14359  txuni2  14435  txopn  14444  upxp  14451  uptx  14453  txrest  14455  hmeoimaf1o  14493  xmettxlem  14688  xmettx  14689  elply2  14914  elplyr  14919  lgslem1  15157  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2d  15226  lgseisenlem2  15228  lgsquadlem2  15235  2lgslem1b  15246  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2lgsoddprmlem2  15263  2sqlem2  15272  2sqlem8  15280  2sqlem9  15281  bj-nn0suc0  15512  bj-inf2vnlem1  15532  bj-nn0sucALT  15540  pwle2  15559  iooref1o  15594