Theorem eqeq2d 2151

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 2149	. 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 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  eqtrd  2172  eq2tri  2199  rspcedeq2vd  2799  rspceeqv  2807  sbceq1g  3022  euabsn  3593  absneu  3595  preq12bg  3700  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab2v  4005  mpteq12f  4008  cbvmptf  4022  cbvmpt  4023  exmidsssn  4125  exmidsssnc  4126  opth  4159  eqvinop  4165  moop2  4173  euotd  4176  eusvnf  4374  reusv3i  4380  nlimsucg  4481  nn0suc  4518  opelxp  4569  elvvv  4602  relop  4689  elrnmpt1s  4789  elrnmpt1  4790  elsnres  4856  elxp4  5026  elxp5  5027  relresfld  5068  iotajust  5087  iota1  5102  iota2df  5112  funopg  5157  funcnvuni  5192  fun11iun  5388  funcocnv2  5392  nfvres  5454  ssimaex  5482  fvmptg  5497  fvmptdf  5508  fvopab6  5517  fmptco  5586  fsng  5593  foco2  5655  elabrex  5659  abrexco  5660  f1veqaeq  5670  dff13f  5671  f1ocnvfv  5680  f1ocnvfvb  5681  fcofo  5685  fliftfun  5697  fliftval  5701  f1oiso2  5728  riota5f  5754  oprabid  5803  rspceov  5813  dfoprab2  5818  mpoeq123dva  5832  mpoeq3dva  5835  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvmpox  5849  mpomptx  5862  ovmpos  5894  ovmpodf  5902  ovmpodv2  5904  ovi3  5907  ov6g  5908  fnrnov  5916  foov  5917  caovcang  5932  caovcan  5935  f1opw2  5976  opabex3d  6019  opabex3  6020  fo1st  6055  fo2nd  6056  elxp6  6067  op1steq  6077  dfoprab4f  6091  fmpox  6098  fnmpoovd  6112  df1st2  6116  df2nd2  6117  xporderlem  6128  cnvoprab  6131  f1od2  6132  brtpos2  6148  dftpos4  6160  tposfn2  6163  recseq  6203  tfr1onlemaccex  6245  tfrcllemaccex  6258  frecabcl  6296  frecsuc  6304  nna0r  6374  eqerlem  6460  qseq2  6478  ecelqsg  6482  snec  6490  qsinxp  6505  ecoptocl  6516  eroveu  6520  th3qlem1  6531  th3qlem2  6532  th3q  6534  mapsncnv  6589  elixpsn  6629  ixpsnf1o  6630  en1  6693  mapsnen  6705  xpsnen  6715  xpassen  6724  xpf1o  6738  mapen  6740  mapxpen  6742  fidifsnen  6764  ac6sfi  6792  undifdc  6812  djuf1olem  6938  djur  6954  updjud  6967  omp1eomlem  6979  0ct  6992  enumctlemm  6999  fodjuomnilemdc  7016  fodjuomni  7021  fodjumkv  7034  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  dfplpq2  7162  dfmpq2  7163  enqbreq2  7165  enq0sym  7240  enq0ref  7241  enq0tr  7242  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  mulnnnq0  7258  nqnq0a  7262  nqnq0m  7263  nq0a0  7265  prarloclemcalc  7310  genipv  7317  genpassl  7332  genpassu  7333  addcomprg  7386  mulcomprg  7388  distrlem1prl  7390  distrlem1pru  7391  distrlem5prl  7394  distrlem5pru  7395  1idprl  7398  1idpru  7399  recexprlem1ssl  7441  recexprlem1ssu  7442  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  elreal  7636  axcnre  7689  axcaucvglemval  7705  negeu  7953  subeq0  7988  apreap  8349  apreim  8365  divmulap3  8437  diveqap0  8442  diveqap1  8465  nn0ind-raph  9168  elq  9414  zq  9418  cnref1o  9440  iccf1o  9787  fzen  9823  fseq1m1p1  9875  fzm1  9880  modqmuladd  10139  modqmuladdnn0  10141  modfzo0difsn  10168  nn0ennn  10206  seq3id2  10282  bcval5  10509  fihashen1  10545  shftlem  10588  shftfvalg  10590  shftfval  10593  negfi  10999  xrmaxiflemcom  11018  xrnegiso  11031  xrnegcon1d  11033  sumeq2  11128  summodc  11152  fsum3  11156  fsum2dlemstep  11203  isumsplit  11260  mertenslemub  11303  mertensabs  11306  prodeq2w  11325  prodeq2  11326  prodmodc  11347  moddvds  11502  dvdsnegb  11510  dvdsabseq  11545  dvdsmod  11560  odd2np1lem  11569  odd2np1  11570  opeo  11594  omeo  11595  divalglemnn  11615  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  bezoutlemnewy  11684  bezoutlema  11687  bezoutlemb  11688  bezoutlemex  11689  bezoutlemaz  11691  bezoutlembz  11692  eucalglt  11738  qredeq  11777  qredeu  11778  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  qnumdenbi  11870  hashgcdlem  11903  evenennn  11906  ennnfonelemim  11937  istopon  12180  eltg3  12226  restsn  12349  txuni2  12425  txopn  12434  upxp  12441  uptx  12443  txrest  12445  hmeoimaf1o  12483  xmettxlem  12678  xmettx  12679  bj-nn0suc0  13148  bj-inf2vnlem1  13168  bj-nn0sucALT  13176  pwle2  13193