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  2852  rspceeqv  2860  sbceq1g  3078  euabsn  3663  absneu  3665  preq12bg  3774  cbvopab  4075  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  cbvopab2v  4081  mpteq12f  4084  cbvmptf  4098  cbvmpt  4099  exmidsssn  4203  exmidsssnc  4204  opth  4238  eqvinop  4244  moop2  4252  euotd  4255  eusvnf  4454  reusv3i  4460  nlimsucg  4566  nn0suc  4604  opelxp  4657  elvvv  4690  relop  4778  elrnmpt1s  4878  elrnmpt1  4879  elsnres  4945  elxp4  5117  elxp5  5118  relresfld  5159  iotajust  5178  iota1  5193  iota2df  5203  funopg  5251  funcnvuni  5286  fun11iun  5483  funcocnv2  5487  nfvres  5549  ssimaex  5578  fvmptg  5593  fvmptdf  5604  fvopab6  5613  fnmptfvd  5621  fmptco  5683  fsng  5690  foco2  5755  elabrex  5759  abrexco  5760  f1veqaeq  5770  dff13f  5771  f1ocnvfv  5780  f1ocnvfvb  5781  fcofo  5785  fliftfun  5797  fliftval  5801  f1oiso2  5828  riota5f  5855  oprabid  5907  rspceov  5917  dfoprab2  5922  mpoeq123dva  5936  mpoeq3dva  5939  cbvoprab1  5947  cbvoprab2  5948  cbvoprab12  5949  cbvmpox  5953  mpomptx  5966  ovmpos  5998  ovmpodf  6006  ovmpodv2  6008  ovi3  6011  ov6g  6012  fnrnov  6020  foov  6021  caovcang  6036  caovcan  6039  f1opw2  6077  opabex3d  6122  opabex3  6123  fo1st  6158  fo2nd  6159  elxp6  6170  op1steq  6180  dfoprab4f  6194  fmpox  6201  fnmpoovd  6216  df1st2  6220  df2nd2  6221  xporderlem  6232  cnvoprab  6235  f1od2  6236  brtpos2  6252  dftpos4  6264  tposfn2  6267  recseq  6307  tfr1onlemaccex  6349  tfrcllemaccex  6362  frecabcl  6400  frecsuc  6408  nna0r  6479  eqerlem  6566  qseq2  6584  ecelqsg  6588  snec  6596  qsinxp  6611  ecoptocl  6622  eroveu  6626  th3qlem1  6637  th3qlem2  6638  th3q  6640  mapsncnv  6695  elixpsn  6735  ixpsnf1o  6736  en1  6799  mapsnen  6811  xpsnen  6821  xpassen  6830  xpf1o  6844  mapen  6846  mapxpen  6848  fidifsnen  6870  ac6sfi  6898  undifdc  6923  djuf1olem  7052  djur  7068  updjud  7081  omp1eomlem  7093  0ct  7106  enumctlemm  7113  fodjuomnilemdc  7142  fodjuomni  7147  fodjumkv  7158  nninfwlporlemd  7170  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  cc2lem  7265  dfplpq2  7353  dfmpq2  7354  enqbreq2  7356  enq0sym  7431  enq0ref  7432  enq0tr  7433  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  mulnnnq0  7449  nqnq0a  7453  nqnq0m  7454  nq0a0  7456  prarloclemcalc  7501  genipv  7508  genpassl  7523  genpassu  7524  addcomprg  7577  mulcomprg  7579  distrlem1prl  7581  distrlem1pru  7582  distrlem5prl  7585  distrlem5pru  7586  1idprl  7589  1idpru  7590  recexprlem1ssl  7632  recexprlem1ssu  7633  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  elreal  7827  axcnre  7880  axcaucvglemval  7896  negeu  8148  subeq0  8183  apreap  8544  apreim  8560  divmulap3  8634  diveqap0  8639  diveqap1  8662  nn0ind-raph  9370  elq  9622  zq  9626  elpq  9648  cnref1o  9650  iccf1o  10004  fzen  10043  fseq1m1p1  10095  fzm1  10100  modqmuladd  10366  modqmuladdnn0  10368  modfzo0difsn  10395  nn0ennn  10433  seq3id2  10509  qsqeqor  10631  bcval5  10743  fihashen1  10779  shftlem  10825  shftfvalg  10827  shftfval  10830  negfi  11236  xrmaxiflemcom  11257  xrnegiso  11270  xrnegcon1d  11272  sumeq2  11367  summodc  11391  fsum3  11395  fsum2dlemstep  11442  isumsplit  11499  mertenslemub  11542  mertensabs  11545  prodeq2w  11564  prodeq2  11565  prodmodc  11586  fprodseq  11591  fprod2dlemstep  11630  moddvds  11806  modm1div  11807  dvdsnegb  11815  dvdsabseq  11853  dvdsmod  11868  odd2np1lem  11877  odd2np1  11878  opeo  11902  omeo  11903  divalglemnn  11923  divalglemeunn  11926  divalglemex  11927  divalglemeuneg  11928  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  bezoutlemex  12002  bezoutlemaz  12004  bezoutlembz  12005  eucalglt  12057  qredeq  12096  qredeu  12097  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  qnumdenbi  12192  hashgcdlem  12238  coprimeprodsq2  12258  pythagtriplem18  12281  pythagtriplem19  12282  pceu  12295  pcval  12296  pczpre  12297  pcdiv  12302  dvdsprmpweq  12334  dvdsprmpweqnn  12335  difsqpwdvds  12337  pcmpt  12341  pcfac  12348  oddprmdvds  12352  4sqlem2  12387  4sqlem3  12388  4sqlem4  12390  evenennn  12394  ennnfonelemim  12425  ptex  12713  intopsn  12786  ismnddef  12819  sgrpidmndm  12821  mndpfo  12839  grpid  12912  grpidrcan  12935  grpidlcan  12936  grplactcnv  12972  srgpcomp  13173  ringadd2  13210  islmod  13381  istopon  13516  eltg3  13560  restsn  13683  txuni2  13759  txopn  13768  upxp  13775  uptx  13777  txrest  13779  hmeoimaf1o  13817  xmettxlem  14012  xmettx  14013  lgslem1  14404  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem2  14454  2lgsoddprmlem2  14457  2sqlem2  14465  2sqlem8  14473  2sqlem9  14474  bj-nn0suc0  14705  bj-inf2vnlem1  14725  bj-nn0sucALT  14733  pwle2  14751  iooref1o  14785