Theorem eqeq2d 2169

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 2167	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C = A <-> C = B ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  eqtrd  2190  eq2tri  2217  rspcedeq2vd  2826  rspceeqv  2834  sbceq1g  3051  euabsn  3629  absneu  3631  preq12bg  3736  cbvopab  4035  cbvopab1  4037  cbvopab2  4038  cbvopab1s  4039  cbvopab2v  4041  mpteq12f  4044  cbvmptf  4058  cbvmpt  4059  exmidsssn  4163  exmidsssnc  4164  opth  4197  eqvinop  4203  moop2  4211  euotd  4214  eusvnf  4413  reusv3i  4419  nlimsucg  4525  nn0suc  4563  opelxp  4616  elvvv  4649  relop  4736  elrnmpt1s  4836  elrnmpt1  4837  elsnres  4903  elxp4  5073  elxp5  5074  relresfld  5115  iotajust  5134  iota1  5149  iota2df  5159  funopg  5204  funcnvuni  5239  fun11iun  5435  funcocnv2  5439  nfvres  5501  ssimaex  5529  fvmptg  5544  fvmptdf  5555  fvopab6  5564  fmptco  5633  fsng  5640  foco2  5704  elabrex  5708  abrexco  5709  f1veqaeq  5719  dff13f  5720  f1ocnvfv  5729  f1ocnvfvb  5730  fcofo  5734  fliftfun  5746  fliftval  5750  f1oiso2  5777  riota5f  5804  oprabid  5853  rspceov  5863  dfoprab2  5868  mpoeq123dva  5882  mpoeq3dva  5885  cbvoprab1  5893  cbvoprab2  5894  cbvoprab12  5895  cbvmpox  5899  mpomptx  5912  ovmpos  5944  ovmpodf  5952  ovmpodv2  5954  ovi3  5957  ov6g  5958  fnrnov  5966  foov  5967  caovcang  5982  caovcan  5985  f1opw2  6026  opabex3d  6069  opabex3  6070  fo1st  6105  fo2nd  6106  elxp6  6117  op1steq  6127  dfoprab4f  6141  fmpox  6148  fnmpoovd  6162  df1st2  6166  df2nd2  6167  xporderlem  6178  cnvoprab  6181  f1od2  6182  brtpos2  6198  dftpos4  6210  tposfn2  6213  recseq  6253  tfr1onlemaccex  6295  tfrcllemaccex  6308  frecabcl  6346  frecsuc  6354  nna0r  6425  eqerlem  6511  qseq2  6529  ecelqsg  6533  snec  6541  qsinxp  6556  ecoptocl  6567  eroveu  6571  th3qlem1  6582  th3qlem2  6583  th3q  6585  mapsncnv  6640  elixpsn  6680  ixpsnf1o  6681  en1  6744  mapsnen  6756  xpsnen  6766  xpassen  6775  xpf1o  6789  mapen  6791  mapxpen  6793  fidifsnen  6815  ac6sfi  6843  undifdc  6868  djuf1olem  6997  djur  7013  updjud  7026  omp1eomlem  7038  0ct  7051  enumctlemm  7058  fodjuomnilemdc  7087  fodjuomni  7092  fodjumkv  7103  exmidfodomrlemeldju  7134  exmidfodomrlemreseldju  7135  cc2lem  7186  dfplpq2  7274  dfmpq2  7275  enqbreq2  7277  enq0sym  7352  enq0ref  7353  enq0tr  7354  addnq0mo  7367  mulnq0mo  7368  addnnnq0  7369  mulnnnq0  7370  nqnq0a  7374  nqnq0m  7375  nq0a0  7377  prarloclemcalc  7422  genipv  7429  genpassl  7444  genpassu  7445  addcomprg  7498  mulcomprg  7500  distrlem1prl  7502  distrlem1pru  7503  distrlem5prl  7506  distrlem5pru  7507  1idprl  7510  1idpru  7511  recexprlem1ssl  7553  recexprlem1ssu  7554  addsrmo  7663  mulsrmo  7664  addsrpr  7665  mulsrpr  7666  elreal  7748  axcnre  7801  axcaucvglemval  7817  negeu  8066  subeq0  8101  apreap  8462  apreim  8478  divmulap3  8550  diveqap0  8555  diveqap1  8578  nn0ind-raph  9281  elq  9531  zq  9535  elpq  9557  cnref1o  9559  iccf1o  9908  fzen  9945  fseq1m1p1  9997  fzm1  10002  modqmuladd  10265  modqmuladdnn0  10267  modfzo0difsn  10294  nn0ennn  10332  seq3id2  10408  bcval5  10637  fihashen1  10673  shftlem  10716  shftfvalg  10718  shftfval  10721  negfi  11127  xrmaxiflemcom  11146  xrnegiso  11159  xrnegcon1d  11161  sumeq2  11256  summodc  11280  fsum3  11284  fsum2dlemstep  11331  isumsplit  11388  mertenslemub  11431  mertensabs  11434  prodeq2w  11453  prodeq2  11454  prodmodc  11475  fprodseq  11480  fprod2dlemstep  11519  moddvds  11695  modm1div  11696  dvdsnegb  11704  dvdsabseq  11739  dvdsmod  11754  odd2np1lem  11763  odd2np1  11764  opeo  11788  omeo  11789  divalglemnn  11809  divalglemeunn  11812  divalglemex  11813  divalglemeuneg  11814  bezoutlemnewy  11880  bezoutlema  11883  bezoutlemb  11884  bezoutlemex  11885  bezoutlemaz  11887  bezoutlembz  11888  eucalglt  11934  qredeq  11973  qredeu  11974  divgcdcoprm0  11978  divgcdcoprmex  11979  cncongr1  11980  cncongr2  11981  qnumdenbi  12067  hashgcdlem  12113  evenennn  12133  ennnfonelemim  12164  istopon  12422  eltg3  12468  restsn  12591  txuni2  12667  txopn  12676  upxp  12683  uptx  12685  txrest  12687  hmeoimaf1o  12725  xmettxlem  12920  xmettx  12921  bj-nn0suc0  13536  bj-inf2vnlem1  13556  bj-nn0sucALT  13564  pwle2  13581  iooref1o  13616