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  3692  absneu  3694  preq12bg  3803  cbvopab  4104  cbvopab1  4106  cbvopab2  4107  cbvopab1s  4108  cbvopab2v  4110  mpteq12f  4113  cbvmptf  4127  cbvmpt  4128  exmidsssn  4235  exmidsssnc  4236  opth  4270  eqvinop  4276  moop2  4284  euotd  4287  eusvnf  4488  reusv3i  4494  nlimsucg  4602  nn0suc  4640  opelxp  4693  elvvv  4726  relop  4816  elrnmpt1s  4916  elrnmpt1  4917  elsnres  4983  elxp4  5157  elxp5  5158  relresfld  5199  iotajust  5218  iota1  5233  iota2df  5244  funopg  5292  funcnvuni  5327  fun11iun  5525  funcocnv2  5529  nfvres  5592  ssimaex  5622  fvmptg  5637  fvmptdf  5649  fvopab6  5658  fnmptfvd  5666  fmptco  5728  fsng  5735  foco2  5800  elabrex  5804  elabrexg  5805  abrexco  5806  f1veqaeq  5816  dff13f  5817  f1ocnvfv  5826  f1ocnvfvb  5827  fcofo  5831  fliftfun  5843  fliftval  5847  f1oiso2  5874  riota5f  5902  oprabid  5954  rspceov  5964  dfoprab2  5969  mpoeq123dva  5983  mpoeq3dva  5986  cbvoprab1  5994  cbvoprab2  5995  cbvoprab12  5996  cbvmpox  6000  mpomptx  6013  ovmpos  6046  ovmpodf  6054  ovmpodv2  6056  ovi3  6060  ov6g  6061  fnrnov  6069  foov  6070  caovcang  6085  caovcan  6088  f1opw2  6129  opabex3d  6178  opabex3  6179  fo1st  6215  fo2nd  6216  elxp6  6227  op1steq  6237  dfoprab4f  6251  fmpox  6258  fnmpoovd  6273  df1st2  6277  df2nd2  6278  xporderlem  6289  cnvoprab  6292  f1od2  6293  brtpos2  6309  dftpos4  6321  tposfn2  6324  recseq  6364  tfr1onlemaccex  6406  tfrcllemaccex  6419  frecabcl  6457  frecsuc  6465  nna0r  6536  eqerlem  6623  qseq2  6643  ecelqsg  6647  snec  6655  qsinxp  6670  ecoptocl  6681  eroveu  6685  th3qlem1  6696  th3qlem2  6697  th3q  6699  mapsncnv  6754  elixpsn  6794  ixpsnf1o  6795  en1  6858  mapsnen  6870  xpsnen  6880  xpassen  6889  pw2f1odclem  6895  xpf1o  6905  mapen  6907  mapxpen  6909  fidifsnen  6931  ac6sfi  6959  undifdc  6985  djuf1olem  7119  djur  7135  updjud  7148  omp1eomlem  7160  0ct  7173  enumctlemm  7180  fodjuomnilemdc  7210  fodjuomni  7215  fodjumkv  7226  nninfwlporlemd  7238  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  cc2lem  7333  dfplpq2  7421  dfmpq2  7422  enqbreq2  7424  enq0sym  7499  enq0ref  7500  enq0tr  7501  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  mulnnnq0  7517  nqnq0a  7521  nqnq0m  7522  nq0a0  7524  prarloclemcalc  7569  genipv  7576  genpassl  7591  genpassu  7592  addcomprg  7645  mulcomprg  7647  distrlem1prl  7649  distrlem1pru  7650  distrlem5prl  7653  distrlem5pru  7654  1idprl  7657  1idpru  7658  recexprlem1ssl  7700  recexprlem1ssu  7701  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  elreal  7895  axcnre  7948  axcaucvglemval  7964  negeu  8217  subeq0  8252  apreap  8614  apreim  8630  divmulap3  8704  diveqap0  8709  diveqap1  8732  nn0ind-raph  9443  elq  9696  zq  9700  elpq  9723  cnref1o  9725  iccf1o  10079  fzen  10118  fseq1m1p1  10170  fzm1  10175  modqmuladd  10458  modqmuladdnn0  10460  modfzo0difsn  10487  nn0ennn  10525  seqf1oglem1  10611  seq3id2  10618  qsqeqor  10742  bcval5  10855  fihashen1  10891  shftlem  10981  shftfvalg  10983  shftfval  10986  negfi  11393  xrmaxiflemcom  11414  xrnegiso  11427  xrnegcon1d  11429  sumeq2  11524  summodc  11548  fsum3  11552  fsum2dlemstep  11599  isumsplit  11656  mertenslemub  11699  mertensabs  11702  prodeq2w  11721  prodeq2  11722  prodmodc  11743  fprodseq  11748  fprod2dlemstep  11787  moddvds  11964  modm1div  11965  dvdsnegb  11973  dvdsabseq  12012  dvdsmod  12027  odd2np1lem  12037  odd2np1  12038  opeo  12062  omeo  12063  divalglemnn  12083  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  bezoutlemnewy  12163  bezoutlema  12166  bezoutlemb  12167  bezoutlemex  12168  bezoutlemaz  12170  bezoutlembz  12171  eucalglt  12225  qredeq  12264  qredeu  12265  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  qnumdenbi  12360  hashgcdlem  12406  coprimeprodsq2  12427  pythagtriplem18  12450  pythagtriplem19  12451  pceu  12464  pcval  12465  pczpre  12466  pcdiv  12471  dvdsprmpweq  12504  dvdsprmpweqnn  12505  difsqpwdvds  12507  pcmpt  12512  pcfac  12519  oddprmdvds  12523  4sqlem2  12558  4sqlem3  12559  4sqlem4  12561  4sqlem12  12571  evenennn  12610  ennnfonelemim  12641  ptex  12935  intopsn  13010  igsumvalx  13032  gsumfzval  13034  gsumpropd  13035  gsumpropd2  13036  gsumress  13038  gsumval2  13040  ismnddef  13059  sgrpidmndm  13061  mndpfo  13079  mhmex  13094  grpid  13171  grpidrcan  13197  grpidlcan  13198  grplactcnv  13234  isghm  13373  f1ghm0to0  13402  conjghm  13406  srgpcomp  13546  ringadd2  13583  rrgval  13818  opprdomnbg  13830  islmod  13847  lss1d  13939  rspsn  14090  expghmap  14163  zndvds0  14206  znf1o  14207  istopon  14249  eltg3  14293  restsn  14416  txuni2  14492  txopn  14501  upxp  14508  uptx  14510  txrest  14512  hmeoimaf1o  14550  xmettxlem  14745  xmettx  14746  elply2  14971  elplyr  14976  dvdsppwf1o  15225  mpodvdsmulf1o  15226  perfectlem2  15236  perfect  15237  lgslem1  15241  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  gausslemma2d  15310  lgseisenlem2  15312  lgsquadlem2  15319  2lgslem1b  15330  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2lgsoddprmlem2  15347  2sqlem2  15356  2sqlem8  15364  2sqlem9  15365  bj-nn0suc0  15596  bj-inf2vnlem1  15616  bj-nn0sucALT  15624  pwle2  15643  iooref1o  15678