Theorem eqeq2d 2219

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 2217	. 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 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  eqtrd  2240  eq2tri  2267  rspcedeq2vd  2894  rspceeqv  2902  sbceq1g  3121  euabsn  3713  absneu  3715  preq12bg  3827  cbvopab  4131  cbvopab1  4133  cbvopab2  4134  cbvopab1s  4135  cbvopab2v  4137  mpteq12f  4140  cbvmptf  4154  cbvmpt  4155  exmidsssn  4262  exmidsssnc  4263  opth  4299  eqvinop  4305  moop2  4314  euotd  4317  eusvnf  4518  reusv3i  4524  nlimsucg  4632  nn0suc  4670  opelxp  4723  elvvv  4756  relop  4846  elrnmpt1s  4947  elrnmpt1  4948  elsnres  5015  elxp4  5189  elxp5  5190  relresfld  5231  iotajust  5250  iota1  5265  iota2df  5276  funopg  5324  funcnvuni  5362  fun11iun  5565  funcocnv2  5569  nfvres  5633  ssimaex  5663  fvmptg  5678  fvmptdf  5690  fvopab6  5699  fnmptfvd  5707  fmptco  5769  fsng  5776  funopsn  5785  foco2  5845  elabrex  5849  elabrexg  5850  abrexco  5851  f1veqaeq  5861  dff13f  5862  f1ocnvfv  5871  f1ocnvfvb  5872  fcofo  5876  fliftfun  5888  fliftval  5892  f1oiso2  5919  riota5f  5947  oprabid  5999  rspceov  6010  dfoprab2  6015  mpoeq123dva  6029  mpoeq3dva  6032  cbvoprab1  6040  cbvoprab2  6041  cbvoprab12  6042  cbvmpox  6046  mpomptx  6059  ovmpos  6092  ovmpodf  6100  ovmpodv2  6102  ovi3  6106  ov6g  6107  fnrnov  6115  foov  6116  caovcang  6131  caovcan  6134  f1opw2  6175  opabex3d  6229  opabex3  6230  fo1st  6266  fo2nd  6267  elxp6  6278  op1steq  6288  dfoprab4f  6302  fmpox  6309  fnmpoovd  6324  df1st2  6328  df2nd2  6329  xporderlem  6340  cnvoprab  6343  f1od2  6344  brtpos2  6360  dftpos4  6372  tposfn2  6375  recseq  6415  tfr1onlemaccex  6457  tfrcllemaccex  6470  frecabcl  6508  frecsuc  6516  nna0r  6587  eqerlem  6674  qseq2  6694  ecelqsg  6698  snec  6706  qsinxp  6721  ecoptocl  6732  eroveu  6736  th3qlem1  6747  th3qlem2  6748  th3q  6750  mapsncnv  6805  elixpsn  6845  ixpsnf1o  6846  en1  6914  mapsnen  6927  en2  6936  xpsnen  6941  xpassen  6950  pw2f1odclem  6956  xpf1o  6966  mapen  6968  mapxpen  6970  fidifsnen  6993  ac6sfi  7021  undifdc  7047  djuf1olem  7181  djur  7197  updjud  7210  omp1eomlem  7222  0ct  7235  enumctlemm  7242  fodjuomnilemdc  7272  fodjuomni  7277  fodjumkv  7288  nninfwlporlemd  7300  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  cc2lem  7413  dfplpq2  7502  dfmpq2  7503  enqbreq2  7505  enq0sym  7580  enq0ref  7581  enq0tr  7582  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  mulnnnq0  7598  nqnq0a  7602  nqnq0m  7603  nq0a0  7605  prarloclemcalc  7650  genipv  7657  genpassl  7672  genpassu  7673  addcomprg  7726  mulcomprg  7728  distrlem1prl  7730  distrlem1pru  7731  distrlem5prl  7734  distrlem5pru  7735  1idprl  7738  1idpru  7739  recexprlem1ssl  7781  recexprlem1ssu  7782  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  elreal  7976  axcnre  8029  axcaucvglemval  8045  negeu  8298  subeq0  8333  apreap  8695  apreim  8711  divmulap3  8785  diveqap0  8790  diveqap1  8813  nn0ind-raph  9525  elq  9778  zq  9782  elpq  9805  cnref1o  9807  iccf1o  10161  fzen  10200  fseq1m1p1  10252  fzm1  10257  modqmuladd  10548  modqmuladdnn0  10550  modfzo0difsn  10577  nn0ennn  10615  seqf1oglem1  10701  seq3id2  10708  qsqeqor  10832  bcval5  10945  fihashen1  10981  wrdl1exs1  11121  wrdl1s1  11122  wrd2ind  11214  swrdccatin2d  11235  reuccatpfxs1lem  11237  shftlem  11242  shftfvalg  11244  shftfval  11247  negfi  11654  xrmaxiflemcom  11675  xrnegiso  11688  xrnegcon1d  11690  sumeq2  11785  summodc  11809  fsum3  11813  fsum2dlemstep  11860  isumsplit  11917  mertenslemub  11960  mertensabs  11963  prodeq2w  11982  prodeq2  11983  prodmodc  12004  fprodseq  12009  fprod2dlemstep  12048  moddvds  12225  modm1div  12226  dvdsnegb  12234  dvdsabseq  12273  dvdsmod  12288  odd2np1lem  12298  odd2np1  12299  opeo  12323  omeo  12324  divalglemnn  12344  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  bitsinv1lem  12387  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  bezoutlemex  12437  bezoutlemaz  12439  bezoutlembz  12440  eucalglt  12494  qredeq  12533  qredeu  12534  divgcdcoprm0  12538  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  qnumdenbi  12629  hashgcdlem  12675  coprimeprodsq2  12696  pythagtriplem18  12719  pythagtriplem19  12720  pceu  12733  pcval  12734  pczpre  12735  pcdiv  12740  dvdsprmpweq  12773  dvdsprmpweqnn  12774  difsqpwdvds  12776  pcmpt  12781  pcfac  12788  oddprmdvds  12792  4sqlem2  12827  4sqlem3  12828  4sqlem4  12830  4sqlem12  12840  evenennn  12879  ennnfonelemim  12910  ptex  13211  intopsn  13314  igsumvalx  13336  gsumfzval  13338  gsumpropd  13339  gsumpropd2  13340  gsumress  13342  gsumval2  13344  ismnddef  13365  sgrpidmndm  13367  mndpfo  13385  mhmex  13409  grpid  13486  grpidrcan  13512  grpidlcan  13513  grplactcnv  13549  isghm  13694  f1ghm0to0  13723  conjghm  13727  srgpcomp  13867  ringadd2  13904  rrgval  14139  opprdomnbg  14151  islmod  14168  lss1d  14260  rspsn  14411  expghmap  14484  zndvds0  14527  znf1o  14528  mplvalcoe  14567  istopon  14600  eltg3  14644  restsn  14767  txuni2  14843  txopn  14852  upxp  14859  uptx  14861  txrest  14863  hmeoimaf1o  14901  xmettxlem  15096  xmettx  15097  elply2  15322  elplyr  15327  dvdsppwf1o  15576  mpodvdsmulf1o  15577  perfectlem2  15587  perfect  15588  lgslem1  15592  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  gausslemma2d  15661  lgseisenlem2  15663  lgsquadlem2  15670  2lgslem1b  15681  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  2lgsoddprmlem2  15698  2sqlem2  15707  2sqlem8  15715  2sqlem9  15716  incistruhgr  15801  upgrex  15814  bj-nn0suc0  16085  bj-inf2vnlem1  16105  bj-nn0sucALT  16113  pwle2  16137  iooref1o  16175