Theorem eqeq2d 2241

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 2239	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtrd  2262  eq2tri  2289  rspcedeq2vd  2917  rspceeqv  2925  sbceq1g  3144  euabsn  3736  absneu  3738  ifpprsnssdc  3774  preq12bg  3851  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  mpteq12f  4164  cbvmptf  4178  cbvmpt  4179  exmidsssn  4286  exmidsssnc  4287  opth  4323  eqvinop  4329  moop2  4338  euotd  4341  eusvnf  4544  reusv3i  4550  nlimsucg  4658  nn0suc  4696  opelxp  4749  elvvv  4782  relop  4872  elrnmpt1s  4974  elrnmpt1  4975  elsnres  5042  elxp4  5216  elxp5  5217  relresfld  5258  iotajust  5277  iota1  5293  iota2df  5304  funopg  5352  funcnvuni  5390  fun11iun  5593  funcocnv2  5597  nfvres  5663  ssimaex  5695  fvmptg  5710  fvmptdf  5722  fvopab6  5731  fnmptfvd  5739  fmptco  5801  fsng  5808  funopsn  5817  foco2  5877  elabrex  5881  elabrexg  5882  abrexco  5883  f1veqaeq  5893  dff13f  5894  f1ocnvfv  5903  f1ocnvfvb  5904  fcofo  5908  fliftfun  5920  fliftval  5924  f1oiso2  5951  riotaeqimp  5979  riota5f  5981  oprabid  6033  rspceov  6044  dfoprab2  6051  mpoeq123dva  6065  mpoeq3dva  6068  cbvoprab1  6076  cbvoprab2  6077  cbvoprab12  6078  cbvmpox  6082  mpomptx  6095  ovmpos  6128  ovmpodf  6136  ovmpodv2  6138  ovi3  6142  ov6g  6143  fnrnov  6151  foov  6152  caovcang  6167  caovcan  6170  f1opw2  6212  opabex3d  6266  opabex3  6267  fo1st  6303  fo2nd  6304  elxp6  6315  op1steq  6325  dfoprab4f  6339  fmpox  6346  fnmpoovd  6361  df1st2  6365  df2nd2  6366  xporderlem  6377  cnvoprab  6380  f1od2  6381  brtpos2  6397  dftpos4  6409  tposfn2  6412  recseq  6452  tfr1onlemaccex  6494  tfrcllemaccex  6507  frecabcl  6545  frecsuc  6553  nna0r  6624  eqerlem  6711  qseq2  6731  ecelqsg  6735  snec  6743  qsinxp  6758  ecoptocl  6769  eroveu  6773  th3qlem1  6784  th3qlem2  6785  th3q  6787  mapsncnv  6842  elixpsn  6882  ixpsnf1o  6883  en1  6951  mapsnen  6964  en2  6973  xpsnen  6980  xpassen  6989  pw2f1odclem  6995  xpf1o  7005  mapen  7007  mapxpen  7009  fidifsnen  7032  ac6sfi  7060  undifdc  7086  djuf1olem  7220  djur  7236  updjud  7249  omp1eomlem  7261  0ct  7274  enumctlemm  7281  fodjuomnilemdc  7311  fodjuomni  7316  fodjumkv  7327  nninfwlporlemd  7339  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  cc2lem  7452  dfplpq2  7541  dfmpq2  7542  enqbreq2  7544  enq0sym  7619  enq0ref  7620  enq0tr  7621  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  mulnnnq0  7637  nqnq0a  7641  nqnq0m  7642  nq0a0  7644  prarloclemcalc  7689  genipv  7696  genpassl  7711  genpassu  7712  addcomprg  7765  mulcomprg  7767  distrlem1prl  7769  distrlem1pru  7770  distrlem5prl  7773  distrlem5pru  7774  1idprl  7777  1idpru  7778  recexprlem1ssl  7820  recexprlem1ssu  7821  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933  elreal  8015  axcnre  8068  axcaucvglemval  8084  negeu  8337  subeq0  8372  apreap  8734  apreim  8750  divmulap3  8824  diveqap0  8829  diveqap1  8852  nn0ind-raph  9564  elq  9817  zq  9821  elpq  9844  cnref1o  9846  iccf1o  10200  fzen  10239  fseq1m1p1  10291  fzm1  10296  modqmuladd  10588  modqmuladdnn0  10590  modfzo0difsn  10617  nn0ennn  10655  seqf1oglem1  10741  seq3id2  10748  qsqeqor  10872  bcval5  10985  fihashen1  11021  wrdl1exs1  11162  wrdl1s1  11163  wrd2ind  11255  swrdccatin2d  11276  reuccatpfxs1lem  11278  shftlem  11327  shftfvalg  11329  shftfval  11332  negfi  11739  xrmaxiflemcom  11760  xrnegiso  11773  xrnegcon1d  11775  sumeq2  11870  summodc  11894  fsum3  11898  fsum2dlemstep  11945  isumsplit  12002  mertenslemub  12045  mertensabs  12048  prodeq2w  12067  prodeq2  12068  prodmodc  12089  fprodseq  12094  fprod2dlemstep  12133  moddvds  12310  modm1div  12311  dvdsnegb  12319  dvdsabseq  12358  dvdsmod  12373  odd2np1lem  12383  odd2np1  12384  opeo  12408  omeo  12409  divalglemnn  12429  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  bitsinv1lem  12472  bezoutlemnewy  12517  bezoutlema  12520  bezoutlemb  12521  bezoutlemex  12522  bezoutlemaz  12524  bezoutlembz  12525  eucalglt  12579  qredeq  12618  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  qnumdenbi  12714  hashgcdlem  12760  coprimeprodsq2  12781  pythagtriplem18  12804  pythagtriplem19  12805  pceu  12818  pcval  12819  pczpre  12820  pcdiv  12825  dvdsprmpweq  12858  dvdsprmpweqnn  12859  difsqpwdvds  12861  pcmpt  12866  pcfac  12873  oddprmdvds  12877  4sqlem2  12912  4sqlem3  12913  4sqlem4  12915  4sqlem12  12925  evenennn  12964  ennnfonelemim  12995  ptex  13297  intopsn  13400  igsumvalx  13422  gsumfzval  13424  gsumpropd  13425  gsumpropd2  13426  gsumress  13428  gsumval2  13430  ismnddef  13451  sgrpidmndm  13453  mndpfo  13471  mhmex  13495  grpid  13572  grpidrcan  13598  grpidlcan  13599  grplactcnv  13635  isghm  13780  f1ghm0to0  13809  conjghm  13813  srgpcomp  13953  ringadd2  13990  rrgval  14226  opprdomnbg  14238  islmod  14255  lss1d  14347  rspsn  14498  expghmap  14571  zndvds0  14614  znf1o  14615  mplvalcoe  14654  istopon  14687  eltg3  14731  restsn  14854  txuni2  14930  txopn  14939  upxp  14946  uptx  14948  txrest  14950  hmeoimaf1o  14988  xmettxlem  15183  xmettx  15184  elply2  15409  elplyr  15414  dvdsppwf1o  15663  mpodvdsmulf1o  15664  perfectlem2  15674  perfect  15675  lgslem1  15679  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  gausslemma2d  15748  lgseisenlem2  15750  lgsquadlem2  15757  2lgslem1b  15768  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2lgsoddprmlem2  15785  2sqlem2  15794  2sqlem8  15802  2sqlem9  15803  incistruhgr  15890  upgrex  15903  usgredg4  16013  usgredgreu  16014  uspgredg2vtxeu  16016  uspgredg2v  16019  usgredg2vlem2  16021  usgredg2v  16022  wlk1walkdom  16070  upgriswlkdc  16071  bj-nn0suc0  16313  bj-inf2vnlem1  16333  bj-nn0sucALT  16341  pwle2  16364  iooref1o  16402