Theorem eqeq2d 2250

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtrd  2271  eq2tri  2298  rspcedeq2vd  2940  rspceeqv  2948  sbceq1g  3167  ifeqeqxdc  3687  euabsn  3781  absneu  3783  ifpprsnssdc  3820  preq12bg  3898  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  mpteq12f  4211  cbvmptf  4225  cbvmpt  4226  exmidsssn  4339  exmidsssnc  4340  opth  4377  eqvinop  4383  moop2  4392  euotd  4395  eusvnf  4599  reusv3i  4605  nlimsucg  4713  nn0suc  4751  opelxp  4804  elvvv  4838  relop  4930  elrnmpt1s  5032  elrnmpt1  5033  elsnres  5100  elxp4  5275  elxp5  5276  relresfld  5317  iotajust  5336  iota1  5352  iota2df  5363  funopg  5411  funcnvuni  5450  fun11iun  5660  funcocnv2  5664  nfvres  5732  ssimaex  5764  fvmptg  5781  fvmptdf  5793  fvopab6  5805  fnmptfvd  5813  fmptco  5874  fsng  5881  fsn2g  5883  funopsn  5891  dfimafnf  5955  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1veqaeq  5975  dff13f  5976  f1ocnvfv  5985  f1ocnvfvb  5986  fcofo  5990  fliftfun  6002  fliftval  6006  f1oiso2  6033  riotaeqimp  6063  riota5f  6065  oprabid  6117  rspceov  6128  dfoprab2  6135  mpoeq123dva  6149  mpoeq3dva  6152  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvmpox  6166  mpomptx  6179  ovmpos  6212  ovmpodf  6220  ovmpodv2  6222  ovi3  6226  ov6g  6227  fnrnov  6235  foov  6236  caovcang  6251  caovcan  6254  f1opw2  6296  opabex3d  6350  opabex3  6351  fo1st  6391  fo2nd  6392  elxp6  6403  op1steq  6413  dfoprab4f  6427  fmpox  6436  fnmpoovd  6451  df1st2  6455  df2nd2  6456  xporderlem  6467  cnvoprab  6470  f1od2  6471  brtpos2  6522  dftpos4  6534  tposfn2  6537  recseq  6577  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecabcl  6670  frecsuc  6678  nna0r  6751  eqerlem  6838  qseq2  6858  ecelqsg  6862  snec  6870  qsinxp  6885  ecoptocl  6896  eroveu  6900  th3qlem1  6911  th3qlem2  6912  th3q  6914  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1  7086  mapsnend  7099  mapsnen  7100  en2  7112  xpsnen  7119  xpassen  7128  pw2f1odclem  7134  xpf1o  7144  mapen  7146  mapxpen  7148  mapunen  7151  fidifsnen  7172  ac6sfi  7202  undifdc  7231  djuf1olem  7393  djur  7409  updjud  7422  omp1eomlem  7434  0ct  7447  enumctlemm  7454  fodjuomnilemdc  7484  fodjuomni  7489  fodjumkv  7500  nninfwlporlemd  7512  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  enqbreq2  7724  enq0sym  7799  enq0ref  7800  enq0tr  7801  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  nqnq0a  7821  nqnq0m  7822  nq0a0  7824  prarloclemcalc  7869  genipv  7876  genpassl  7891  genpassu  7892  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  1idprl  7957  1idpru  7958  recexprlem1ssl  8000  recexprlem1ssu  8001  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  elreal  8195  axcnre  8248  axcaucvglemval  8264  negeu  8517  subeq0  8552  apreap  8915  apreim  8931  divmulap3  9007  diveqap0  9012  diveqap1  9035  nn0ind-raph  9763  elq  10022  zq  10026  elpq  10049  cnref1o  10051  iccf1o  10407  fzen  10447  fseq1m1p1  10502  fzm1  10507  modqmuladd  10803  modqmuladdnn0  10805  modfzo0difsn  10832  nn0ennn  10870  seqf1oglem1  10956  seq3id2  10963  qsqeqor  11087  bcval5  11201  fihashen1  11238  hashf1lem1  11285  wrdl1exs1  11397  wrdl1s1  11398  wrd2ind  11495  swrdccatin2d  11516  reuccatpfxs1lem  11518  shftlem  11581  shftfvalg  11583  shftfval  11586  negfi  11994  xrmaxiflemcom  12015  xrnegiso  12028  xrnegcon1d  12030  sumeq2  12125  summodc  12150  fsum3  12154  fsum2dlemstep  12201  isumsplit  12258  mertenslemub  12301  mertensabs  12304  prodeq2w  12323  prodeq2  12324  prodmodc  12345  fprodseq  12350  fprod2dlemstep  12389  moddvds  12566  modm1div  12567  dvdsnegb  12575  dvdsabseq  12614  dvdsmod  12629  odd2np1lem  12639  odd2np1  12640  opeo  12664  omeo  12665  divalglemnn  12685  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  bitsinv1lem  12728  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  bezoutlemex  12778  bezoutlemaz  12780  bezoutlembz  12781  eucalglt  12835  qredeq  12874  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  qnumdenbi  12970  hashgcdlem  13016  coprimeprodsq2  13037  pythagtriplem18  13060  pythagtriplem19  13061  pceu  13074  pcval  13075  pczpre  13076  pcdiv  13081  dvdsprmpweq  13114  dvdsprmpweqnn  13115  difsqpwdvds  13117  pcmpt  13122  pcfac  13129  oddprmdvds  13133  4sqlem2  13168  4sqlem3  13169  4sqlem4  13171  4sqlem12  13181  ballotfilemfc0  13232  ballotfilemfcc  13233  evenennn  13284  ennnfonelemim  13315  ptex  13618  intopsn  13687  gzsumvalx  13709  gzsumfzval  13711  gzsumress  13712  gzsumval2  13714  ismnddef  13731  sgrpidmndm  13733  mndpfo  13751  mhmex  13769  grpid  13844  grpidrcan  13870  grpidlcan  13871  grplactcnv  13907  isghm  14046  f1ghm0to0  14075  conjghm  14079  gsumvalfi  14152  srgpcomp  14294  ringadd2  14332  rrgval  14570  opprdomnbg  14583  islmod  14627  lss1d  14720  rspsn  14871  expghmap  14942  zndvds0  14985  znf1o  14986  psrbagconf1o  15064  mplvalcoe  15081  istopon  15114  eltg3  15158  restsn  15281  txuni2  15357  txopn  15366  upxp  15373  uptx  15375  txrest  15377  hmeoimaf1o  15415  xmettxlem  15610  xmettx  15611  elply2  15836  elplyr  15841  dvdsppwf1o  16103  mpodvdsmulf1o  16104  perfectlem2  16114  perfect  16115  lgslem1  16119  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  gausslemma2d  16188  lgseisenlem2  16190  lgsquadlem2  16197  2lgslem1b  16208  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2lgsoddprmlem2  16225  2sqlem2  16234  2sqlem8  16242  2sqlem9  16243  incistruhgr  16331  upgrex  16344  usgredg4  16456  usgredgreu  16457  uspgredg2vtxeu  16459  uspgredg2v  16462  usgredg2vlem2  16464  usgredg2v  16465  vtxdgfifival  16532  vtxdumgrfival  16539  1loopgrvd2fi  16546  wlk1walkdom  16600  upgriswlkdc  16601  eupth2lem3lem3fi  16711  eupth2fi  16720  bj-nn0suc0  16976  bj-inf2vnlem1  16996  bj-nn0sucALT  17004  pwle2  17028  iooref1o  17083  qdiff  17098