Theorem eqeq2d 2189

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 2187	. 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 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtrd  2210  eq2tri  2237  rspcedeq2vd  2851  rspceeqv  2859  sbceq1g  3077  euabsn  3662  absneu  3664  preq12bg  3772  cbvopab  4072  cbvopab1  4074  cbvopab2  4075  cbvopab1s  4076  cbvopab2v  4078  mpteq12f  4081  cbvmptf  4095  cbvmpt  4096  exmidsssn  4200  exmidsssnc  4201  opth  4235  eqvinop  4241  moop2  4249  euotd  4252  eusvnf  4451  reusv3i  4457  nlimsucg  4563  nn0suc  4601  opelxp  4654  elvvv  4687  relop  4774  elrnmpt1s  4874  elrnmpt1  4875  elsnres  4941  elxp4  5113  elxp5  5114  relresfld  5155  iotajust  5174  iota1  5189  iota2df  5199  funopg  5247  funcnvuni  5282  fun11iun  5479  funcocnv2  5483  nfvres  5545  ssimaex  5574  fvmptg  5589  fvmptdf  5600  fvopab6  5609  fnmptfvd  5617  fmptco  5679  fsng  5686  foco2  5750  elabrex  5754  abrexco  5755  f1veqaeq  5765  dff13f  5766  f1ocnvfv  5775  f1ocnvfvb  5776  fcofo  5780  fliftfun  5792  fliftval  5796  f1oiso2  5823  riota5f  5850  oprabid  5902  rspceov  5912  dfoprab2  5917  mpoeq123dva  5931  mpoeq3dva  5934  cbvoprab1  5942  cbvoprab2  5943  cbvoprab12  5944  cbvmpox  5948  mpomptx  5961  ovmpos  5993  ovmpodf  6001  ovmpodv2  6003  ovi3  6006  ov6g  6007  fnrnov  6015  foov  6016  caovcang  6031  caovcan  6034  f1opw2  6072  opabex3d  6117  opabex3  6118  fo1st  6153  fo2nd  6154  elxp6  6165  op1steq  6175  dfoprab4f  6189  fmpox  6196  fnmpoovd  6211  df1st2  6215  df2nd2  6216  xporderlem  6227  cnvoprab  6230  f1od2  6231  brtpos2  6247  dftpos4  6259  tposfn2  6262  recseq  6302  tfr1onlemaccex  6344  tfrcllemaccex  6357  frecabcl  6395  frecsuc  6403  nna0r  6474  eqerlem  6561  qseq2  6579  ecelqsg  6583  snec  6591  qsinxp  6606  ecoptocl  6617  eroveu  6621  th3qlem1  6632  th3qlem2  6633  th3q  6635  mapsncnv  6690  elixpsn  6730  ixpsnf1o  6731  en1  6794  mapsnen  6806  xpsnen  6816  xpassen  6825  xpf1o  6839  mapen  6841  mapxpen  6843  fidifsnen  6865  ac6sfi  6893  undifdc  6918  djuf1olem  7047  djur  7063  updjud  7076  omp1eomlem  7088  0ct  7101  enumctlemm  7108  fodjuomnilemdc  7137  fodjuomni  7142  fodjumkv  7153  nninfwlporlemd  7165  exmidfodomrlemeldju  7193  exmidfodomrlemreseldju  7194  cc2lem  7260  dfplpq2  7348  dfmpq2  7349  enqbreq2  7351  enq0sym  7426  enq0ref  7427  enq0tr  7428  addnq0mo  7441  mulnq0mo  7442  addnnnq0  7443  mulnnnq0  7444  nqnq0a  7448  nqnq0m  7449  nq0a0  7451  prarloclemcalc  7496  genipv  7503  genpassl  7518  genpassu  7519  addcomprg  7572  mulcomprg  7574  distrlem1prl  7576  distrlem1pru  7577  distrlem5prl  7580  distrlem5pru  7581  1idprl  7584  1idpru  7585  recexprlem1ssl  7627  recexprlem1ssu  7628  addsrmo  7737  mulsrmo  7738  addsrpr  7739  mulsrpr  7740  elreal  7822  axcnre  7875  axcaucvglemval  7891  negeu  8142  subeq0  8177  apreap  8538  apreim  8554  divmulap3  8628  diveqap0  8633  diveqap1  8656  nn0ind-raph  9364  elq  9616  zq  9620  elpq  9642  cnref1o  9644  iccf1o  9998  fzen  10036  fseq1m1p1  10088  fzm1  10093  modqmuladd  10359  modqmuladdnn0  10361  modfzo0difsn  10388  nn0ennn  10426  seq3id2  10502  qsqeqor  10623  bcval5  10734  fihashen1  10770  shftlem  10816  shftfvalg  10818  shftfval  10821  negfi  11227  xrmaxiflemcom  11248  xrnegiso  11261  xrnegcon1d  11263  sumeq2  11358  summodc  11382  fsum3  11386  fsum2dlemstep  11433  isumsplit  11490  mertenslemub  11533  mertensabs  11536  prodeq2w  11555  prodeq2  11556  prodmodc  11577  fprodseq  11582  fprod2dlemstep  11621  moddvds  11797  modm1div  11798  dvdsnegb  11806  dvdsabseq  11843  dvdsmod  11858  odd2np1lem  11867  odd2np1  11868  opeo  11892  omeo  11893  divalglemnn  11913  divalglemeunn  11916  divalglemex  11917  divalglemeuneg  11918  bezoutlemnewy  11987  bezoutlema  11990  bezoutlemb  11991  bezoutlemex  11992  bezoutlemaz  11994  bezoutlembz  11995  eucalglt  12047  qredeq  12086  qredeu  12087  divgcdcoprm0  12091  divgcdcoprmex  12092  cncongr1  12093  cncongr2  12094  qnumdenbi  12182  hashgcdlem  12228  coprimeprodsq2  12248  pythagtriplem18  12271  pythagtriplem19  12272  pceu  12285  pcval  12286  pczpre  12287  pcdiv  12292  dvdsprmpweq  12324  dvdsprmpweqnn  12325  difsqpwdvds  12327  pcmpt  12331  pcfac  12338  oddprmdvds  12342  4sqlem2  12377  4sqlem3  12378  4sqlem4  12380  evenennn  12384  ennnfonelemim  12415  intopsn  12716  ismnddef  12749  sgrpidmndm  12751  mndpfo  12769  grpid  12840  grpidrcan  12863  grpidlcan  12864  grplactcnv  12900  srgpcomp  13073  ringadd2  13110  istopon  13293  eltg3  13339  restsn  13462  txuni2  13538  txopn  13547  upxp  13554  uptx  13556  txrest  13558  hmeoimaf1o  13596  xmettxlem  13791  xmettx  13792  lgslem1  14183  lgsdirnn0  14230  lgsdinn0  14231  2sqlem2  14233  2sqlem8  14241  2sqlem9  14242  bj-nn0suc0  14473  bj-inf2vnlem1  14493  bj-nn0sucALT  14501  pwle2  14519  iooref1o  14553