Theorem eqeq2d 2217

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 2215	. 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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqtrd  2238  eq2tri  2265  rspcedeq2vd  2887  rspceeqv  2895  sbceq1g  3113  euabsn  3703  absneu  3705  preq12bg  3814  cbvopab  4116  cbvopab1  4118  cbvopab2  4119  cbvopab1s  4120  cbvopab2v  4122  mpteq12f  4125  cbvmptf  4139  cbvmpt  4140  exmidsssn  4247  exmidsssnc  4248  opth  4282  eqvinop  4288  moop2  4297  euotd  4300  eusvnf  4501  reusv3i  4507  nlimsucg  4615  nn0suc  4653  opelxp  4706  elvvv  4739  relop  4829  elrnmpt1s  4929  elrnmpt1  4930  elsnres  4997  elxp4  5171  elxp5  5172  relresfld  5213  iotajust  5232  iota1  5247  iota2df  5258  funopg  5306  funcnvuni  5344  fun11iun  5545  funcocnv2  5549  nfvres  5612  ssimaex  5642  fvmptg  5657  fvmptdf  5669  fvopab6  5678  fnmptfvd  5686  fmptco  5748  fsng  5755  funopsn  5764  foco2  5824  elabrex  5828  elabrexg  5829  abrexco  5830  f1veqaeq  5840  dff13f  5841  f1ocnvfv  5850  f1ocnvfvb  5851  fcofo  5855  fliftfun  5867  fliftval  5871  f1oiso2  5898  riota5f  5926  oprabid  5978  rspceov  5989  dfoprab2  5994  mpoeq123dva  6008  mpoeq3dva  6011  cbvoprab1  6019  cbvoprab2  6020  cbvoprab12  6021  cbvmpox  6025  mpomptx  6038  ovmpos  6071  ovmpodf  6079  ovmpodv2  6081  ovi3  6085  ov6g  6086  fnrnov  6094  foov  6095  caovcang  6110  caovcan  6113  f1opw2  6154  opabex3d  6208  opabex3  6209  fo1st  6245  fo2nd  6246  elxp6  6257  op1steq  6267  dfoprab4f  6281  fmpox  6288  fnmpoovd  6303  df1st2  6307  df2nd2  6308  xporderlem  6319  cnvoprab  6322  f1od2  6323  brtpos2  6339  dftpos4  6351  tposfn2  6354  recseq  6394  tfr1onlemaccex  6436  tfrcllemaccex  6449  frecabcl  6487  frecsuc  6495  nna0r  6566  eqerlem  6653  qseq2  6673  ecelqsg  6677  snec  6685  qsinxp  6700  ecoptocl  6711  eroveu  6715  th3qlem1  6726  th3qlem2  6727  th3q  6729  mapsncnv  6784  elixpsn  6824  ixpsnf1o  6825  en1  6893  mapsnen  6905  en2  6914  xpsnen  6918  xpassen  6927  pw2f1odclem  6933  xpf1o  6943  mapen  6945  mapxpen  6947  fidifsnen  6969  ac6sfi  6997  undifdc  7023  djuf1olem  7157  djur  7173  updjud  7186  omp1eomlem  7198  0ct  7211  enumctlemm  7218  fodjuomnilemdc  7248  fodjuomni  7253  fodjumkv  7264  nninfwlporlemd  7276  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  cc2lem  7380  dfplpq2  7469  dfmpq2  7470  enqbreq2  7472  enq0sym  7547  enq0ref  7548  enq0tr  7549  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  mulnnnq0  7565  nqnq0a  7569  nqnq0m  7570  nq0a0  7572  prarloclemcalc  7617  genipv  7624  genpassl  7639  genpassu  7640  addcomprg  7693  mulcomprg  7695  distrlem1prl  7697  distrlem1pru  7698  distrlem5prl  7701  distrlem5pru  7702  1idprl  7705  1idpru  7706  recexprlem1ssl  7748  recexprlem1ssu  7749  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  elreal  7943  axcnre  7996  axcaucvglemval  8012  negeu  8265  subeq0  8300  apreap  8662  apreim  8678  divmulap3  8752  diveqap0  8757  diveqap1  8780  nn0ind-raph  9492  elq  9745  zq  9749  elpq  9772  cnref1o  9774  iccf1o  10128  fzen  10167  fseq1m1p1  10219  fzm1  10224  modqmuladd  10513  modqmuladdnn0  10515  modfzo0difsn  10542  nn0ennn  10580  seqf1oglem1  10666  seq3id2  10673  qsqeqor  10797  bcval5  10910  fihashen1  10946  wrdl1exs1  11086  wrdl1s1  11087  shftlem  11160  shftfvalg  11162  shftfval  11165  negfi  11572  xrmaxiflemcom  11593  xrnegiso  11606  xrnegcon1d  11608  sumeq2  11703  summodc  11727  fsum3  11731  fsum2dlemstep  11778  isumsplit  11835  mertenslemub  11878  mertensabs  11881  prodeq2w  11900  prodeq2  11901  prodmodc  11922  fprodseq  11927  fprod2dlemstep  11966  moddvds  12143  modm1div  12144  dvdsnegb  12152  dvdsabseq  12191  dvdsmod  12206  odd2np1lem  12216  odd2np1  12217  opeo  12241  omeo  12242  divalglemnn  12262  divalglemeunn  12265  divalglemex  12266  divalglemeuneg  12267  bitsinv1lem  12305  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  bezoutlemex  12355  bezoutlemaz  12357  bezoutlembz  12358  eucalglt  12412  qredeq  12451  qredeu  12452  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  qnumdenbi  12547  hashgcdlem  12593  coprimeprodsq2  12614  pythagtriplem18  12637  pythagtriplem19  12638  pceu  12651  pcval  12652  pczpre  12653  pcdiv  12658  dvdsprmpweq  12691  dvdsprmpweqnn  12692  difsqpwdvds  12694  pcmpt  12699  pcfac  12706  oddprmdvds  12710  4sqlem2  12745  4sqlem3  12746  4sqlem4  12748  4sqlem12  12758  evenennn  12797  ennnfonelemim  12828  ptex  13129  intopsn  13232  igsumvalx  13254  gsumfzval  13256  gsumpropd  13257  gsumpropd2  13258  gsumress  13260  gsumval2  13262  ismnddef  13283  sgrpidmndm  13285  mndpfo  13303  mhmex  13327  grpid  13404  grpidrcan  13430  grpidlcan  13431  grplactcnv  13467  isghm  13612  f1ghm0to0  13641  conjghm  13645  srgpcomp  13785  ringadd2  13822  rrgval  14057  opprdomnbg  14069  islmod  14086  lss1d  14178  rspsn  14329  expghmap  14402  zndvds0  14445  znf1o  14446  mplvalcoe  14485  istopon  14518  eltg3  14562  restsn  14685  txuni2  14761  txopn  14770  upxp  14777  uptx  14779  txrest  14781  hmeoimaf1o  14819  xmettxlem  15014  xmettx  15015  elply2  15240  elplyr  15245  dvdsppwf1o  15494  mpodvdsmulf1o  15495  perfectlem2  15505  perfect  15506  lgslem1  15510  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  gausslemma2d  15579  lgseisenlem2  15581  lgsquadlem2  15588  2lgslem1b  15599  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610  2lgsoddprmlem2  15616  2sqlem2  15625  2sqlem8  15633  2sqlem9  15634  bj-nn0suc0  15923  bj-inf2vnlem1  15943  bj-nn0sucALT  15951  pwle2  15972  iooref1o  16010