Theorem eqeq2d 2242

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 2240	. 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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2212

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

This theorem is referenced by:  eqtrd  2263  eq2tri  2290  rspcedeq2vd  2919  rspceeqv  2927  sbceq1g  3146  euabsn  3742  absneu  3744  ifpprsnssdc  3780  preq12bg  3857  cbvopab  4161  cbvopab1  4163  cbvopab2  4164  cbvopab1s  4165  cbvopab2v  4167  mpteq12f  4170  cbvmptf  4184  cbvmpt  4185  exmidsssn  4294  exmidsssnc  4295  opth  4331  eqvinop  4337  moop2  4346  euotd  4349  eusvnf  4552  reusv3i  4558  nlimsucg  4666  nn0suc  4704  opelxp  4757  elvvv  4791  relop  4882  elrnmpt1s  4984  elrnmpt1  4985  elsnres  5052  elxp4  5226  elxp5  5227  relresfld  5268  iotajust  5287  iota1  5303  iota2df  5314  funopg  5362  funcnvuni  5401  fun11iun  5607  funcocnv2  5611  nfvres  5678  ssimaex  5710  fvmptg  5725  fvmptdf  5737  fvopab6  5746  fnmptfvd  5754  fmptco  5816  fsng  5823  fsn2g  5825  funopsn  5833  foco2  5899  elabrex  5903  elabrexg  5904  abrexco  5905  f1veqaeq  5915  dff13f  5916  f1ocnvfv  5925  f1ocnvfvb  5926  fcofo  5930  fliftfun  5942  fliftval  5946  f1oiso2  5973  riotaeqimp  6001  riota5f  6003  oprabid  6055  rspceov  6066  dfoprab2  6073  mpoeq123dva  6087  mpoeq3dva  6090  cbvoprab1  6098  cbvoprab2  6099  cbvoprab12  6100  cbvmpox  6104  mpomptx  6117  ovmpos  6150  ovmpodf  6158  ovmpodv2  6160  ovi3  6164  ov6g  6165  fnrnov  6173  foov  6174  caovcang  6189  caovcan  6192  f1opw2  6234  opabex3d  6288  opabex3  6289  fo1st  6325  fo2nd  6326  elxp6  6337  op1steq  6347  dfoprab4f  6361  fmpox  6370  fnmpoovd  6385  df1st2  6389  df2nd2  6390  xporderlem  6401  cnvoprab  6404  f1od2  6405  brtpos2  6422  dftpos4  6434  tposfn2  6437  recseq  6477  tfr1onlemaccex  6519  tfrcllemaccex  6532  frecabcl  6570  frecsuc  6578  nna0r  6651  eqerlem  6738  qseq2  6758  ecelqsg  6762  snec  6770  qsinxp  6785  ecoptocl  6796  eroveu  6800  th3qlem1  6811  th3qlem2  6812  th3q  6814  mapsncnv  6869  elixpsn  6909  ixpsnf1o  6910  en1  6978  mapsnen  6991  en2  7003  xpsnen  7010  xpassen  7019  pw2f1odclem  7025  xpf1o  7035  mapen  7037  mapxpen  7039  fidifsnen  7062  ac6sfi  7092  undifdc  7121  djuf1olem  7257  djur  7273  updjud  7286  omp1eomlem  7298  0ct  7311  enumctlemm  7318  fodjuomnilemdc  7348  fodjuomni  7353  fodjumkv  7364  nninfwlporlemd  7376  exmidfodomrlemeldju  7415  exmidfodomrlemreseldju  7416  cc2lem  7490  dfplpq2  7579  dfmpq2  7580  enqbreq2  7582  enq0sym  7657  enq0ref  7658  enq0tr  7659  addnq0mo  7672  mulnq0mo  7673  addnnnq0  7674  mulnnnq0  7675  nqnq0a  7679  nqnq0m  7680  nq0a0  7682  prarloclemcalc  7727  genipv  7734  genpassl  7749  genpassu  7750  addcomprg  7803  mulcomprg  7805  distrlem1prl  7807  distrlem1pru  7808  distrlem5prl  7811  distrlem5pru  7812  1idprl  7815  1idpru  7816  recexprlem1ssl  7858  recexprlem1ssu  7859  addsrmo  7968  mulsrmo  7969  addsrpr  7970  mulsrpr  7971  elreal  8053  axcnre  8106  axcaucvglemval  8122  negeu  8375  subeq0  8410  apreap  8772  apreim  8788  divmulap3  8862  diveqap0  8867  diveqap1  8890  nn0ind-raph  9602  elq  9861  zq  9865  elpq  9888  cnref1o  9890  iccf1o  10244  fzen  10283  fseq1m1p1  10335  fzm1  10340  modqmuladd  10634  modqmuladdnn0  10636  modfzo0difsn  10663  nn0ennn  10701  seqf1oglem1  10787  seq3id2  10794  qsqeqor  10918  bcval5  11031  fihashen1  11067  wrdl1exs1  11215  wrdl1s1  11216  wrd2ind  11313  swrdccatin2d  11334  reuccatpfxs1lem  11336  shftlem  11399  shftfvalg  11401  shftfval  11404  negfi  11811  xrmaxiflemcom  11832  xrnegiso  11845  xrnegcon1d  11847  sumeq2  11942  summodc  11967  fsum3  11971  fsum2dlemstep  12018  isumsplit  12075  mertenslemub  12118  mertensabs  12121  prodeq2w  12140  prodeq2  12141  prodmodc  12162  fprodseq  12167  fprod2dlemstep  12206  moddvds  12383  modm1div  12384  dvdsnegb  12392  dvdsabseq  12431  dvdsmod  12446  odd2np1lem  12456  odd2np1  12457  opeo  12481  omeo  12482  divalglemnn  12502  divalglemeunn  12505  divalglemex  12506  divalglemeuneg  12507  bitsinv1lem  12545  bezoutlemnewy  12590  bezoutlema  12593  bezoutlemb  12594  bezoutlemex  12595  bezoutlemaz  12597  bezoutlembz  12598  eucalglt  12652  qredeq  12691  qredeu  12692  divgcdcoprm0  12696  divgcdcoprmex  12697  cncongr1  12698  cncongr2  12699  qnumdenbi  12787  hashgcdlem  12833  coprimeprodsq2  12854  pythagtriplem18  12877  pythagtriplem19  12878  pceu  12891  pcval  12892  pczpre  12893  pcdiv  12898  dvdsprmpweq  12931  dvdsprmpweqnn  12932  difsqpwdvds  12934  pcmpt  12939  pcfac  12946  oddprmdvds  12950  4sqlem2  12985  4sqlem3  12986  4sqlem4  12988  4sqlem12  12998  evenennn  13037  ennnfonelemim  13068  ptex  13370  intopsn  13473  igsumvalx  13495  gsumfzval  13497  gsumpropd  13498  gsumpropd2  13499  gsumress  13501  gsumval2  13503  ismnddef  13524  sgrpidmndm  13526  mndpfo  13544  mhmex  13568  grpid  13645  grpidrcan  13671  grpidlcan  13672  grplactcnv  13708  isghm  13853  f1ghm0to0  13882  conjghm  13886  srgpcomp  14027  ringadd2  14064  rrgval  14300  opprdomnbg  14312  islmod  14329  lss1d  14421  rspsn  14572  expghmap  14645  zndvds0  14688  znf1o  14689  psrbagconf1o  14716  mplvalcoe  14733  istopon  14766  eltg3  14810  restsn  14933  txuni2  15009  txopn  15018  upxp  15025  uptx  15027  txrest  15029  hmeoimaf1o  15067  xmettxlem  15262  xmettx  15263  elply2  15488  elplyr  15493  dvdsppwf1o  15742  mpodvdsmulf1o  15743  perfectlem2  15753  perfect  15754  lgslem1  15758  lgsdirnn0  15805  lgsdinn0  15806  gausslemma2dlem0i  15815  gausslemma2dlem1a  15816  gausslemma2d  15827  lgseisenlem2  15829  lgsquadlem2  15836  2lgslem1b  15847  2lgslem3a1  15855  2lgslem3b1  15856  2lgslem3c1  15857  2lgslem3d1  15858  2lgsoddprmlem2  15864  2sqlem2  15873  2sqlem8  15881  2sqlem9  15882  incistruhgr  15970  upgrex  15983  usgredg4  16095  usgredgreu  16096  uspgredg2vtxeu  16098  uspgredg2v  16101  usgredg2vlem2  16103  usgredg2v  16104  vtxdgfifival  16171  vtxdumgrfival  16178  1loopgrvd2fi  16185  wlk1walkdom  16239  upgriswlkdc  16240  eupth2lem3lem3fi  16350  eupth2fi  16359  bj-nn0suc0  16605  bj-inf2vnlem1  16625  bj-nn0sucALT  16633  pwle2  16659  iooref1o  16705  qdiff  16720  gfsumval  16748