Theorem eqeq2d 2177

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  eqtrd  2198  eq2tri  2225  rspcedeq2vd  2839  rspceeqv  2847  sbceq1g  3064  euabsn  3645  absneu  3647  preq12bg  3752  cbvopab  4052  cbvopab1  4054  cbvopab2  4055  cbvopab1s  4056  cbvopab2v  4058  mpteq12f  4061  cbvmptf  4075  cbvmpt  4076  exmidsssn  4180  exmidsssnc  4181  opth  4214  eqvinop  4220  moop2  4228  euotd  4231  eusvnf  4430  reusv3i  4436  nlimsucg  4542  nn0suc  4580  opelxp  4633  elvvv  4666  relop  4753  elrnmpt1s  4853  elrnmpt1  4854  elsnres  4920  elxp4  5090  elxp5  5091  relresfld  5132  iotajust  5151  iota1  5166  iota2df  5176  funopg  5221  funcnvuni  5256  fun11iun  5452  funcocnv2  5456  nfvres  5518  ssimaex  5546  fvmptg  5561  fvmptdf  5572  fvopab6  5581  fmptco  5650  fsng  5657  foco2  5721  elabrex  5725  abrexco  5726  f1veqaeq  5736  dff13f  5737  f1ocnvfv  5746  f1ocnvfvb  5747  fcofo  5751  fliftfun  5763  fliftval  5767  f1oiso2  5794  riota5f  5821  oprabid  5870  rspceov  5880  dfoprab2  5885  mpoeq123dva  5899  mpoeq3dva  5902  cbvoprab1  5910  cbvoprab2  5911  cbvoprab12  5912  cbvmpox  5916  mpomptx  5929  ovmpos  5961  ovmpodf  5969  ovmpodv2  5971  ovi3  5974  ov6g  5975  fnrnov  5983  foov  5984  caovcang  5999  caovcan  6002  f1opw2  6043  opabex3d  6086  opabex3  6087  fo1st  6122  fo2nd  6123  elxp6  6134  op1steq  6144  dfoprab4f  6158  fmpox  6165  fnmpoovd  6179  df1st2  6183  df2nd2  6184  xporderlem  6195  cnvoprab  6198  f1od2  6199  brtpos2  6215  dftpos4  6227  tposfn2  6230  recseq  6270  tfr1onlemaccex  6312  tfrcllemaccex  6325  frecabcl  6363  frecsuc  6371  nna0r  6442  eqerlem  6528  qseq2  6546  ecelqsg  6550  snec  6558  qsinxp  6573  ecoptocl  6584  eroveu  6588  th3qlem1  6599  th3qlem2  6600  th3q  6602  mapsncnv  6657  elixpsn  6697  ixpsnf1o  6698  en1  6761  mapsnen  6773  xpsnen  6783  xpassen  6792  xpf1o  6806  mapen  6808  mapxpen  6810  fidifsnen  6832  ac6sfi  6860  undifdc  6885  djuf1olem  7014  djur  7030  updjud  7043  omp1eomlem  7055  0ct  7068  enumctlemm  7075  fodjuomnilemdc  7104  fodjuomni  7109  fodjumkv  7120  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  cc2lem  7203  dfplpq2  7291  dfmpq2  7292  enqbreq2  7294  enq0sym  7369  enq0ref  7370  enq0tr  7371  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  mulnnnq0  7387  nqnq0a  7391  nqnq0m  7392  nq0a0  7394  prarloclemcalc  7439  genipv  7446  genpassl  7461  genpassu  7462  addcomprg  7515  mulcomprg  7517  distrlem1prl  7519  distrlem1pru  7520  distrlem5prl  7523  distrlem5pru  7524  1idprl  7527  1idpru  7528  recexprlem1ssl  7570  recexprlem1ssu  7571  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  elreal  7765  axcnre  7818  axcaucvglemval  7834  negeu  8085  subeq0  8120  apreap  8481  apreim  8497  divmulap3  8569  diveqap0  8574  diveqap1  8597  nn0ind-raph  9304  elq  9556  zq  9560  elpq  9582  cnref1o  9584  iccf1o  9936  fzen  9974  fseq1m1p1  10026  fzm1  10031  modqmuladd  10297  modqmuladdnn0  10299  modfzo0difsn  10326  nn0ennn  10364  seq3id2  10440  qsqeqor  10561  bcval5  10672  fihashen1  10708  shftlem  10754  shftfvalg  10756  shftfval  10759  negfi  11165  xrmaxiflemcom  11186  xrnegiso  11199  xrnegcon1d  11201  sumeq2  11296  summodc  11320  fsum3  11324  fsum2dlemstep  11371  isumsplit  11428  mertenslemub  11471  mertensabs  11474  prodeq2w  11493  prodeq2  11494  prodmodc  11515  fprodseq  11520  fprod2dlemstep  11559  moddvds  11735  modm1div  11736  dvdsnegb  11744  dvdsabseq  11781  dvdsmod  11796  odd2np1lem  11805  odd2np1  11806  opeo  11830  omeo  11831  divalglemnn  11851  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  bezoutlemex  11930  bezoutlemaz  11932  bezoutlembz  11933  eucalglt  11985  qredeq  12024  qredeu  12025  divgcdcoprm0  12029  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  qnumdenbi  12120  hashgcdlem  12166  coprimeprodsq2  12186  pythagtriplem18  12209  pythagtriplem19  12210  pceu  12223  pcval  12224  pczpre  12225  pcdiv  12230  dvdsprmpweq  12262  dvdsprmpweqnn  12263  difsqpwdvds  12265  pcmpt  12269  pcfac  12276  oddprmdvds  12280  4sqlem2  12315  4sqlem3  12316  4sqlem4  12318  evenennn  12322  ennnfonelemim  12353  istopon  12611  eltg3  12657  restsn  12780  txuni2  12856  txopn  12865  upxp  12872  uptx  12874  txrest  12876  hmeoimaf1o  12914  xmettxlem  13109  xmettx  13110  lgslem1  13501  lgsdirnn0  13548  lgsdinn0  13549  2sqlem2  13551  2sqlem8  13559  2sqlem9  13560  bj-nn0suc0  13792  bj-inf2vnlem1  13812  bj-nn0sucALT  13820  pwle2  13838  iooref1o  13873