Theorem eqeq2d 2217

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 2215	. 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 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqtrd  2238  eq2tri  2265  rspcedeq2vd  2887  rspceeqv  2895  sbceq1g  3113  euabsn  3703  absneu  3705  preq12bg  3814  cbvopab  4115  cbvopab1  4117  cbvopab2  4118  cbvopab1s  4119  cbvopab2v  4121  mpteq12f  4124  cbvmptf  4138  cbvmpt  4139  exmidsssn  4246  exmidsssnc  4247  opth  4281  eqvinop  4287  moop2  4296  euotd  4299  eusvnf  4500  reusv3i  4506  nlimsucg  4614  nn0suc  4652  opelxp  4705  elvvv  4738  relop  4828  elrnmpt1s  4928  elrnmpt1  4929  elsnres  4996  elxp4  5170  elxp5  5171  relresfld  5212  iotajust  5231  iota1  5246  iota2df  5257  funopg  5305  funcnvuni  5343  fun11iun  5543  funcocnv2  5547  nfvres  5610  ssimaex  5640  fvmptg  5655  fvmptdf  5667  fvopab6  5676  fnmptfvd  5684  fmptco  5746  fsng  5753  funopsn  5762  foco2  5822  elabrex  5826  elabrexg  5827  abrexco  5828  f1veqaeq  5838  dff13f  5839  f1ocnvfv  5848  f1ocnvfvb  5849  fcofo  5853  fliftfun  5865  fliftval  5869  f1oiso2  5896  riota5f  5924  oprabid  5976  rspceov  5987  dfoprab2  5992  mpoeq123dva  6006  mpoeq3dva  6009  cbvoprab1  6017  cbvoprab2  6018  cbvoprab12  6019  cbvmpox  6023  mpomptx  6036  ovmpos  6069  ovmpodf  6077  ovmpodv2  6079  ovi3  6083  ov6g  6084  fnrnov  6092  foov  6093  caovcang  6108  caovcan  6111  f1opw2  6152  opabex3d  6206  opabex3  6207  fo1st  6243  fo2nd  6244  elxp6  6255  op1steq  6265  dfoprab4f  6279  fmpox  6286  fnmpoovd  6301  df1st2  6305  df2nd2  6306  xporderlem  6317  cnvoprab  6320  f1od2  6321  brtpos2  6337  dftpos4  6349  tposfn2  6352  recseq  6392  tfr1onlemaccex  6434  tfrcllemaccex  6447  frecabcl  6485  frecsuc  6493  nna0r  6564  eqerlem  6651  qseq2  6671  ecelqsg  6675  snec  6683  qsinxp  6698  ecoptocl  6709  eroveu  6713  th3qlem1  6724  th3qlem2  6725  th3q  6727  mapsncnv  6782  elixpsn  6822  ixpsnf1o  6823  en1  6891  mapsnen  6903  en2  6912  xpsnen  6916  xpassen  6925  pw2f1odclem  6931  xpf1o  6941  mapen  6943  mapxpen  6945  fidifsnen  6967  ac6sfi  6995  undifdc  7021  djuf1olem  7155  djur  7171  updjud  7184  omp1eomlem  7196  0ct  7209  enumctlemm  7216  fodjuomnilemdc  7246  fodjuomni  7251  fodjumkv  7262  nninfwlporlemd  7274  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  cc2lem  7378  dfplpq2  7467  dfmpq2  7468  enqbreq2  7470  enq0sym  7545  enq0ref  7546  enq0tr  7547  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  mulnnnq0  7563  nqnq0a  7567  nqnq0m  7568  nq0a0  7570  prarloclemcalc  7615  genipv  7622  genpassl  7637  genpassu  7638  addcomprg  7691  mulcomprg  7693  distrlem1prl  7695  distrlem1pru  7696  distrlem5prl  7699  distrlem5pru  7700  1idprl  7703  1idpru  7704  recexprlem1ssl  7746  recexprlem1ssu  7747  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  elreal  7941  axcnre  7994  axcaucvglemval  8010  negeu  8263  subeq0  8298  apreap  8660  apreim  8676  divmulap3  8750  diveqap0  8755  diveqap1  8778  nn0ind-raph  9490  elq  9743  zq  9747  elpq  9770  cnref1o  9772  iccf1o  10126  fzen  10165  fseq1m1p1  10217  fzm1  10222  modqmuladd  10511  modqmuladdnn0  10513  modfzo0difsn  10540  nn0ennn  10578  seqf1oglem1  10664  seq3id2  10671  qsqeqor  10795  bcval5  10908  fihashen1  10944  wrdl1exs1  11083  wrdl1s1  11084  shftlem  11127  shftfvalg  11129  shftfval  11132  negfi  11539  xrmaxiflemcom  11560  xrnegiso  11573  xrnegcon1d  11575  sumeq2  11670  summodc  11694  fsum3  11698  fsum2dlemstep  11745  isumsplit  11802  mertenslemub  11845  mertensabs  11848  prodeq2w  11867  prodeq2  11868  prodmodc  11889  fprodseq  11894  fprod2dlemstep  11933  moddvds  12110  modm1div  12111  dvdsnegb  12119  dvdsabseq  12158  dvdsmod  12173  odd2np1lem  12183  odd2np1  12184  opeo  12208  omeo  12209  divalglemnn  12229  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  bitsinv1lem  12272  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  bezoutlemex  12322  bezoutlemaz  12324  bezoutlembz  12325  eucalglt  12379  qredeq  12418  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  qnumdenbi  12514  hashgcdlem  12560  coprimeprodsq2  12581  pythagtriplem18  12604  pythagtriplem19  12605  pceu  12618  pcval  12619  pczpre  12620  pcdiv  12625  dvdsprmpweq  12658  dvdsprmpweqnn  12659  difsqpwdvds  12661  pcmpt  12666  pcfac  12673  oddprmdvds  12677  4sqlem2  12712  4sqlem3  12713  4sqlem4  12715  4sqlem12  12725  evenennn  12764  ennnfonelemim  12795  ptex  13096  intopsn  13199  igsumvalx  13221  gsumfzval  13223  gsumpropd  13224  gsumpropd2  13225  gsumress  13227  gsumval2  13229  ismnddef  13250  sgrpidmndm  13252  mndpfo  13270  mhmex  13294  grpid  13371  grpidrcan  13397  grpidlcan  13398  grplactcnv  13434  isghm  13579  f1ghm0to0  13608  conjghm  13612  srgpcomp  13752  ringadd2  13789  rrgval  14024  opprdomnbg  14036  islmod  14053  lss1d  14145  rspsn  14296  expghmap  14369  zndvds0  14412  znf1o  14413  mplvalcoe  14452  istopon  14485  eltg3  14529  restsn  14652  txuni2  14728  txopn  14737  upxp  14744  uptx  14746  txrest  14748  hmeoimaf1o  14786  xmettxlem  14981  xmettx  14982  elply2  15207  elplyr  15212  dvdsppwf1o  15461  mpodvdsmulf1o  15462  perfectlem2  15472  perfect  15473  lgslem1  15477  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  gausslemma2d  15546  lgseisenlem2  15548  lgsquadlem2  15555  2lgslem1b  15566  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2lgsoddprmlem2  15583  2sqlem2  15592  2sqlem8  15600  2sqlem9  15601  bj-nn0suc0  15886  bj-inf2vnlem1  15906  bj-nn0sucALT  15914  pwle2  15935  iooref1o  15973